If `Maybe a` is `Just a` or `Nothing`, then Erlang's `ok` or `{error, Reason}` should be called `Surely`.

Follow

```
inductive Maybe (R: Type u) where
| just (ok: R)
| nothing

inductive Surely (L: Type u) where
| ok
| error (err: L)
```

Sign in to participate in the conversation
Doma Social

Mastodon server of https://doma.dev.