max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
24019 commits 1 branch 0 tags 5.3 GiB
Commit graph

43 commits

Author SHA1 Message Date
Leonardo de Moura
d77f335ff0 feat: add LawfulMonad instance for ExceptT 2021-02-20 17:01:27 -08:00
Sebastian Ullrich
187a614575 chore: make tryFinally a def 2021-02-17 12:04:20 +01:00
Leonardo de Moura
f57c184dbd chore: remove = true old workarounds 
@Kha The old `= true` workarounds are not needed anymore, they were
due to another issue and are not related to yesterday's issue.
That is, the one exposed by the `ForIn` typeclass.
 2021-02-05 13:48:03 -08:00
Sebastian Ullrich
0c91b3769e chore: replace variables in src/ 2021-01-22 14:36:05 +01:00
Leonardo de Moura
2e11c3bdff feat: dependencies 2020-12-18 11:21:30 -08:00
Leonardo de Moura
16003871e4 feat: add helper instance 2020-11-28 19:01:54 -08:00
Leonardo de Moura
0869f38de4 chore: update structure, class, inductive 2020-11-27 15:09:30 -08:00
Leonardo de Moura
f456e006dc chore: test instance ... where 2020-11-23 18:24:23 -08:00
Leonardo de Moura
e6215f7282 chore: remove some unnecessary commas 2020-11-20 15:47:27 -08:00
Leonardo de Moura
304c80d610 feat: use <| 2020-11-19 09:03:38 -08:00
Leonardo de Moura
6ab0be952c chore: merge src/Control files 
Some of them were almost empty after the refactoring.
 2020-11-10 18:47:23 -08:00
Leonardo de Moura
a8c791ecae chore: remove dead files and functions 
Remove obsolete combinators: `whenM`, `unlessM`, and `condM`

cc @Kha
 2020-11-10 18:37:15 -08:00
Leonardo de Moura
cca3bad0bb feat: add Prelude.lean 
`Prelude.lean` has no dependencies, and
at the end of `Prelude`, the `syntax` and `macro` commands are operational.
 2020-11-10 18:08:18 -08:00
Leonardo de Moura
898a08a0c1 chore: avoid Has prefix in type classes 
closes #203
 2020-10-27 18:29:19 -07:00
Leonardo de Moura
5fed774461 chore: HasRepr ==> Repr 2020-10-27 16:15:10 -07:00
Leonardo de Moura
10c32fcf94 chore: HasToString => ToString 2020-10-27 16:11:48 -07:00
Leonardo de Moura
13c2a8ff51 chore: remove #lang lean4 header 2020-10-25 09:54:07 -07:00
Leonardo de Moura
7030dc91f2 chore: move to new frontend 2020-10-23 12:50:03 -07:00
Leonardo de Moura
a0b8f13094 chore: remove temporary def 2020-10-22 17:42:25 -07:00
Leonardo de Moura
d4a67baa8e refactor: rename MonadFinally.finally' => MonadFinally.tryFinally' 2020-10-22 17:40:30 -07:00
Leonardo de Moura
f1dd85e8a3 chore: remove temporary defs 2020-10-22 17:31:07 -07:00
Leonardo de Moura
02521397ac refactor: rename MonadExceptOf.catch => MonadExceptOf.tryCatch 2020-10-22 17:27:15 -07:00
Leonardo de Moura
a37e2ae46f refactor: simplify MonadFunctor 2020-10-22 17:05:34 -07:00
Leonardo de Moura
fa3c32d3b1 chore: remove adaptExcept 2020-10-22 16:56:23 -07:00
Leonardo de Moura
c865abb340 refactor: remove MonadRun 2020-10-22 16:30:06 -07:00
Leonardo de Moura
749e2063cf feat: add interpolated string for toString 2020-10-09 14:38:24 -07:00
Leonardo de Moura
5efa628e43 chore: split Lift.lean into MonadLift.lean, MonadFunctor.lean, and MonadRun.lean 2020-08-26 08:34:35 -07:00
Leonardo de Moura
321719b300 feat: add MonadFinally 2020-08-25 17:58:35 -07:00
Leonardo de Moura
1103806ff4 refactor: HasMonadLift ==> MonadLift 2020-08-25 13:54:41 -07:00
Leonardo de Moura
b03cd748cf feat: add MonadControl 2020-08-25 13:54:41 -07:00
Leonardo de Moura
916b395d1b chore: cleanup 2020-08-21 09:29:09 -07:00
Leonardo de Moura
6c234daad7 chore: MonadExceptCore => MonadExceptOf 2020-08-13 09:28:23 -07:00
Leonardo de Moura
d7add53229 feat: add MonadExceptCore 2020-08-13 09:19:26 -07:00
Sebastian Ullrich
719819bf49 fix: finally shouldn't call finalizer when finalizer throws 2020-07-10 07:42:26 -07:00
Leonardo de Moura
50990b99d6 chore: remove unnecessary annotations 2020-05-12 15:02:03 -07:00
Leonardo de Moura
33a10130cf chore: fix stdlib 2020-05-12 15:02:03 -07:00
Sebastian Ullrich
8f67db0101 refactor: never implicitly ignore monadic results 
Also change `do e; f` to desugar to `e *> f` so that it is affected as well
 2020-04-23 11:09:59 -07:00
Daniel Selsam
fd61812b6e fix: wrong instance order for several instances 2020-04-08 16:55:48 -07:00
Leonardo de Moura
05fcb9b4d4 chore: remove MonadFail 2020-02-10 13:54:27 -08:00
Leonardo de Moura
22c42ec1d8 chore: remove unnecessary method 2020-01-28 08:24:35 -08:00
Leonardo de Moura
d37d02b512 fix: more general instance 2020-01-01 09:16:29 -08:00
Leonardo de Moura
90178dc3d9 feat: add syntaxNodeKindExtension 
It contains all `SyntaxNodeKind`s registered in the system.
 2019-12-31 16:36:50 -08:00
Leonardo de Moura
c445199747 chore: library/Init ==> src/Init 
cc @Kha @dselsam @cipher1024
 2019-11-22 06:06:05 -08:00
Renamed from library/Init/Control/Except.lean (Browse further)