lean4-htt/src/Init
Leonardo de Moura 5b76155318 feat: new return semantics
`return e` is not equivalent to `pure e` anymore.
Now, `return e` means "return value `e` as the result of the root `do` block".
2020-10-07 14:07:58 -07:00
..
Control chore: add helper instance 2020-10-05 11:24:35 -07:00
Data chore: remove forInMap 2020-10-07 10:01:04 -07:00
System fix: #eval was not capturing dbgTrace! output in pure code 2020-10-05 10:22:04 -07:00
Coe.lean feat: add coeId instance 2020-09-06 08:27:26 -07:00
Control.lean chore: split Lift.lean into MonadLift.lean, MonadFunctor.lean, and MonadRun.lean 2020-08-26 08:34:35 -07:00
Core.lean feat: new return semantics 2020-10-07 14:07:58 -07:00
Data.lean chore: move RBTree and RBMap to Std 2020-06-25 13:26:16 -07:00
Fix.lean
HasCoe.lean chore: remove coeSortBool 2020-01-28 19:07:02 -08:00
LeanInit.lean feat: allow trailing ; at doSeqBracketed 2020-09-26 14:20:47 -07:00
System.lean
Util.lean feat: expand helper macros 2020-09-10 14:25:07 -07:00
WF.lean chore: remove unnecessary annotations 2020-05-12 15:02:03 -07:00