Leonardo de Moura
|
04e3f21783
|
chore: add OptionM monad
Motivation: `Option` is data, `OptionM` is control.
|
2021-03-20 17:50:45 -07:00 |
|
Leonardo de Moura
|
339a4cf740
|
chore: remove defaultInstance for ToString
|
2020-12-19 19:10:42 -08:00 |
|
Leonardo de Moura
|
5f6e66a53f
|
refactor: Repr
Modifications:
- Result type is `Format`
- It takes the context precedence like Haskell `Show`
|
2020-12-18 11:21:30 -08:00 |
|
Leonardo de Moura
|
2e11c3bdff
|
feat: dependencies
|
2020-12-18 11:21:30 -08:00 |
|
Leonardo de Moura
|
40bfafdadb
|
refactor: dependencies
|
2020-12-18 11:21:30 -08:00 |
|
Leonardo de Moura
|
5b588b5984
|
fix: defaultInstance priorities
|
2020-12-16 06:52:55 -08:00 |
|
Leonardo de Moura
|
0869f38de4
|
chore: update structure, class, inductive
|
2020-11-27 15:09:30 -08:00 |
|
Leonardo de Moura
|
b672e37bcc
|
chore: annotate OfNat and ToString default instances
|
2020-11-21 08:34:45 -08:00 |
|
Leonardo de Moura
|
db5fe843de
|
chore: add expandInterpolatedStr helper function, rename msg! => m!
|
2020-11-14 13:52:52 -08:00 |
|
Leonardo de Moura
|
8c4ac7ccc1
|
refactor: rename LeanInit ==> Meta, and reduce dependencies
|
2020-11-13 16:00:31 -08:00 |
|
Leonardo de Moura
|
65dafaf07c
|
fix: stdlib and tests
We also declare a few macros for the syntax command.
|
2020-11-12 07:12:30 -08:00 |
|
Leonardo de Moura
|
6858cb5fb6
|
chore: cleanup
|
2020-10-29 10:24:16 -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
|
f57201d787
|
feat: add Repr and HasToString instances for PUnit and ULift
|
2020-10-12 11:01:59 -07:00 |
|
Leonardo de Moura
|
749e2063cf
|
feat: add interpolated string for toString
|
2020-10-09 14:38:24 -07:00 |
|