Gabriel Ebner
|
1c8ef51124
|
fix: make List.toString tail-recursive
|
2022-12-12 22:58:21 +01:00 |
|
Henrik Böving
|
24cc6eae6d
|
feat: log2 for Fin and UInts
|
2022-11-29 01:05:06 +01:00 |
|
Sebastian Ullrich
|
fb2a2b3de2
|
fix: fixup previous commit
|
2022-06-07 16:37:45 -07:00 |
|
Sebastian Ullrich
|
ae7b895f7a
|
refactor: unname some unused variables
|
2022-06-07 16:37:45 -07:00 |
|
Leonardo de Moura
|
c65537aea5
|
feat: Option is a Monad again
TODO: remove `OptionM` after update stage0
see: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Do.20we.20still.20need.20OptionM.3F/near/279761084
|
2022-05-04 15:27:42 -07:00 |
|
Leonardo de Moura
|
3862e7867b
|
refactor: make String.Pos opaque
TODO: this refactoring exposed bugs in `FuzzyMatching` and `Lake`
closes #410
|
2022-03-20 10:47:13 -07:00 |
|
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 |
|