Commit Graph

8 Commits

Author SHA1 Message Date
Denis Buzdalov
5266a2bc22 [ base ] Implement MonadError () for MaybeT 2022-09-01 10:48:15 +01:00
G. Allais
21c6f4fb79
[ breaking ] remove parsing of dangling binders (#1711)
* [ breaking ] remove parsing of dangling binders

It used to be the case that

```
ID : Type -> Type
ID a = a

test : ID (a : Type) -> a -> a
test = \ a, x => x
```

and

```
head : List $ a -> Maybe a
head [] = Nothing
head (x :: _) = Just x
```

were accepted but these are now rejected because:

* `ID (a : Type) -> a -> a` is parsed as `(ID (a : Type)) -> a -> a`
* `List $ a -> Maybe a` is parsed as `List (a -> Maybe a)`

Similarly if you want to use a lambda / rewrite / let expression as
part of the last argument of an application, the use of `$` or parens
is now mandatory.

This should hopefully allow us to make progress on #1703
2021-08-10 19:24:32 +01:00
Fabián Heredia Montiel
dad4dcdaf8 Add totality annotations to src and libs/{prelude, base} 2021-06-12 21:06:08 -05:00
stefan-hoeck
8cb2220e58 implemented cps-style Writer 2021-01-19 14:34:15 +01:00
stefan-hoeck
b2e7384a80 implemented cps-style RWST 2021-01-19 13:58:18 +01:00
stefan-hoeck
81efdd7992 implementations for MonadError 2021-01-19 12:35:05 +01:00
stefan-hoeck
124afd89b1 moved transformer impls to their own directory 2021-01-19 11:53:23 +01:00
stefan-hoeck
b926e13b96 new transformer layout 2021-01-19 11:45:54 +01:00