Wojciech Nawrocki
e3d866bc03
feat: initial TraceExplorer
...
Motivation: trace messages from systems such as instance synthesis or defeq checks can be massive and it is hard to find the relevant info within. We provide an interactive TraceExplorer component to do this.
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
7babcc2425
fix: tail-recursion in Format pretty-printer
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
77365abc8b
chore: Repr Syntax and minor cleanup
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
bc8027cdc6
perf: speed up String.intercalate
2021-08-24 08:57:41 -07:00
Wojciech Nawrocki
528283bc7d
feat: MonadPrettyFormat
2021-08-24 08:57:41 -07:00
Leonardo de Moura
4dccaa963b
feat: add List.mapTR and csimp lemma
2021-08-22 09:32:19 -07:00
Leonardo de Moura
ec6af1ba26
feat: use simple List.append definition and add csimp theorem
2021-08-21 16:11:54 -07:00
Leonardo de Moura
3b240d9a14
feat: use simple List.length definition and add csimp theorem
2021-08-21 13:11:06 -07:00
Leonardo de Moura
7066619123
refactor: define Nat.le using inductive type
2021-08-20 19:39:45 -07:00
Leonardo de Moura
33a0da8c6f
chore: remove simp annotation from PUnit.eq_punit
...
closes #635
2021-08-19 11:22:13 -07:00
Leonardo de Moura
107712f8be
feat: add instance from CoeSort to CoeTail
2021-08-18 20:24:43 -07:00
Leonardo de Moura
8d90872d28
chore: add not_not_intro
2021-08-17 21:32:32 -07:00
Leonardo de Moura
7c5ab8b4c9
chore: prepare to add <- as simp argument
2021-08-14 06:59:55 -07:00
Leonardo de Moura
25344453c0
feat: add simpStar parser
2021-08-14 06:29:26 -07:00
Leonardo de Moura
a15a36b8d3
chore: cleanup Subarray instances
2021-08-13 19:29:09 -07:00
Leonardo de Moura
4b58c4cc02
refactor: instances that "hide" coercions
...
Example:
```
instance [CoeHTCT α β] [Add β] : HAdd α β β where
hAdd a b := Add.add a b
```
2021-08-13 17:18:55 -07:00
Leonardo de Moura
ef46b0145b
chore: use binop% to define the notations >> and <|>
...
Motivation: we want to delete the instances
```
instance [CoeHTCT α β] [OrElse β] : HOrElse α β β where
hOrElse a b := OrElse.orElse a b
instance [CoeHTCT α β] [OrElse β] : HOrElse β α β where
hOrElse a b := OrElse.orElse a b
instance [CoeHTCT α β] [AndThen β] : HAndThen α β β where
hAndThen a b := AndThen.andThen a b
instance [CoeHTCT α β] [AndThen β] : HAndThen β α β where
hAndThen a b := AndThen.andThen a b
```
after we update stage0
2021-08-13 17:13:01 -07:00
Leonardo de Moura
b012050917
chore: remove some macros that use binop%
...
For example, given `i : Int` and `n : Nat`, we don't want to coerce `n`
into a `Int` in the term `i ^ n`.
2021-08-13 17:00:59 -07:00
Leonardo de Moura
be23709737
chore: use binop% to define ++ notation
2021-08-13 16:26:35 -07:00
Leonardo de Moura
24fe2875c6
chore: change Pow class
...
Based on the suggestion at https://github.com/leanprover/lean4/issues/433
2021-08-12 13:59:55 -07:00
Sebastian Ullrich
6c220423ed
chore: adjust stx precedences
2021-08-12 07:48:42 -07:00
Daniel Selsam
040141f137
feat: unexpander for Subtype
2021-08-12 09:32:33 +02:00
Leonardo de Moura
f4433f3147
feat: add Alternative (StateRefT' ω σ m)
2021-08-10 14:27:05 -07:00
François G. Dorais
358a129d78
fix: protect rfl
2021-08-07 13:25:54 -07:00
Leonardo de Moura
9cc94296e5
chore: remove staging workaround theorems
2021-08-07 12:52:31 -07:00
Leonardo de Moura
a821dcbff2
chore: enforce naming convention for theorems
...
see issue #402
fix: `ElabTerm.lean`
2021-08-07 12:48:38 -07:00
Leonardo de Moura
8a84532760
feat: add PEmpty
...
closes #537
2021-08-06 19:18:22 -07:00
Leonardo de Moura
a230fe2d06
fix: forallMetaTelescope issue
...
This commit incorporates the fix at PR #612 , and clean up
`Meta/Basic.lean` using Lean 4 features.
2021-08-06 09:47:10 -07:00
Leonardo de Moura
4dbb3e6db1
fix: add workaround to prevent code explosion at deriving for FromJson
...
fixes #569
2021-08-05 06:58:07 -07:00
Daniel Selsam
0036111db9
feat: pp.analyze original mvars are not unknown
2021-08-03 09:13:18 +02:00
Daniel Selsam
db4d33487a
fix: unexpanders can't specify exact names
2021-08-03 09:13:18 +02:00
Daniel Selsam
9744b51c1b
fix: unexpand pairs
2021-08-03 09:13:18 +02:00
Daniel Selsam
b3bb82ee7e
feat: turn more delaborators into unexpanders
2021-08-03 09:13:18 +02:00
Daniel Selsam
89364b802b
feat: top-down heuristic delaboration
2021-08-03 09:13:18 +02:00
Leonardo de Moura
ea37a29e4c
chore: remove TODO
2021-08-02 20:25:29 -07:00
Leonardo de Moura
cfb7e27b87
fix: isStructure vs isStructureLike
2021-08-02 18:54:19 -07:00
Wojciech Nawrocki
f1b4d9a193
chore: restore non-generic Format
...
Motivation: it is unclear whether this is the best solution for embedding objects in pretty-printer outputs.
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
b022a7c1d2
style: indent
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
9b8e44618d
chore: default to Format Nat
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
a937fa26ba
chore: fewer explicit types
2021-08-01 09:58:44 +02:00
Wojciech Nawrocki
f51b80060d
feat: generic tagged Format
2021-08-01 09:58:44 +02:00
Leonardo de Moura
af5ff9ceb2
refactor: move List.takeWhile to Init.Data.List.Basic
...
Motivation: make sure it will be aligned by BinPort
2021-07-31 15:03:33 -07:00
Leonardo de Moura
2c037c3989
chore: fix proofs
2021-07-29 16:59:47 -07:00
Leonardo de Moura
f10c27dfb7
perf: add workaround for perf issue
...
See issue #361
2021-07-29 08:29:09 -07:00
Leonardo de Moura
3b5e762882
chore: add temporary workaround
2021-07-27 14:23:05 -07:00
Leonardo de Moura
b986bde639
fix: IO.Error.alreadyExists may have an optional file name
...
We got an assertion violation yesterday at `leanpkg` at
```cpp
case EEXIST: case EINPROGRESS: case EISCONN:
lean_assert(fname == nullptr); // <<<<<<< HERE
return lean_mk_io_error_already_exists(errnum, details);
```
2021-07-27 07:00:06 -07:00
Wojciech Nawrocki
f27a069773
chore: drop UntypedRef and use monotonic RpcRefs
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
776a0c71aa
feat: add UInt64 unpackings
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
b3d9e90695
feat: IO.getRandomBytes
2021-07-24 10:45:28 +02:00
Wojciech Nawrocki
85dcdcde93
chore: use NonScalar
2021-07-24 10:45:28 +02:00
