Leonardo de Moura
|
1941081059
|
chore: update stage0
|
2021-01-29 18:25:17 -08:00 |
|
Leonardo de Moura
|
d71aab5dc4
|
fix: allow bigger ctor objects
`IR/Checker.lean` is now also checking the maximum number of fields
and scalar size
|
2021-01-29 18:23:38 -08:00 |
|
Leonardo de Moura
|
bd65035cbb
|
chore: update stage0
|
2021-01-29 17:19:12 -08:00 |
|
Leonardo de Moura
|
3c02f877a8
|
chore: fix test
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
761b64c929
|
fix: missing occursCheck at SyntheticMVars
fixes #301
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
bf77f0707e
|
refactor: remove no-mutual workaround
This is still leftover from the old frontend.
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
920ae5f1b9
|
chore: cleanup
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
3b2605018b
|
fix: propagate nested LCtx at elimMVar
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
32f219772c
|
chore: minor
|
2021-01-29 17:13:04 -08:00 |
|
Leonardo de Moura
|
e102cd4f42
|
fix: checkAssignment must be at assignConst
Example of issue fixed by this commit: the variables `xs` may have references to `mvar`.
|
2021-01-29 17:13:03 -08:00 |
|
Leonardo de Moura
|
c86803392e
|
refactor: withNestedTraces
|
2021-01-29 17:13:03 -08:00 |
|
Leonardo de Moura
|
8699f439da
|
chore: avoid big match-expr
|
2021-01-29 17:13:03 -08:00 |
|
Leonardo de Moura
|
07beb6bc46
|
chore: cleanup
|
2021-01-29 17:13:03 -08:00 |
|
Leonardo de Moura
|
af7db05000
|
chore: remove nested outParam
|
2021-01-29 17:13:03 -08:00 |
|
Sebastian Ullrich
|
811b90dd0e
|
feat: option for disabling hygiene
/cc @leodemoura
|
2021-01-29 15:26:06 +01:00 |
|
Leonardo de Moura
|
5a02c4facc
|
chore: cleanup
|
2021-01-28 15:23:46 -08:00 |
|
Leonardo de Moura
|
27a27d33d2
|
feat: special cases for mkCongrArg, mkCongrFun, mkCongr
|
2021-01-28 12:19:56 -08:00 |
|
Leonardo de Moura
|
1d76f3e1c1
|
chore: cleanup
|
2021-01-28 12:03:06 -08:00 |
|
Wojciech Nawrocki
|
28d6a1ebe1
|
fix: go-to-def paths on Windows
|
2021-01-28 11:45:33 -08:00 |
|
Leonardo de Moura
|
8115dd11c8
|
chore: update stage0
|
2021-01-28 11:38:26 -08:00 |
|
Leonardo de Moura
|
d7ca646071
|
fix: make sure mkUnit return Syntax that is a valid term and pattern
|
2021-01-28 11:27:28 -08:00 |
|
Leonardo de Moura
|
51699f3a5b
|
feat: ensure binder names are atomic
|
2021-01-28 11:27:28 -08:00 |
|
Sebastian Ullrich
|
434564b125
|
chore: clean up manual From/ToJson instances
|
2021-01-28 15:51:47 +01:00 |
|
Sebastian Ullrich
|
d8b13c0fa2
|
chore: update stage0
|
2021-01-28 15:09:24 +01:00 |
|
Sebastian Ullrich
|
f3f31052e5
|
fix: From/ToJson derive handlers with inheritance
|
2021-01-28 15:07:26 +01:00 |
|
Leonardo de Moura
|
870896ba45
|
chore: fix test
|
2021-01-27 18:40:53 -08:00 |
|
Leonardo de Moura
|
7f047a95f4
|
chore: update stage0
|
2021-01-27 18:35:34 -08:00 |
|
Leonardo de Moura
|
4a19a5d2a4
|
refactor: move Eq.trans to Prelude.lean
We need it at `SizeOf.lean`
|
2021-01-27 18:27:04 -08:00 |
|
Leonardo de Moura
|
70d6ea57a2
|
fix: mkSizeOfSpecLemmaInstance
It was not handling correctly constructors with implicit fields.
|
2021-01-27 18:24:32 -08:00 |
|
Leonardo de Moura
|
f1a0044241
|
fix: use previously generated sizeOf_spec lemmas to expand rhs
|
2021-01-27 18:14:25 -08:00 |
|
Leonardo de Moura
|
c47c25cf33
|
feat: finish sizeOf_spec lemma generation
|
2021-01-27 17:20:23 -08:00 |
|
Leonardo de Moura
|
46d861847e
|
chore: update stage0
|
2021-01-27 16:28:01 -08:00 |
|
Leonardo de Moura
|
7d4f80fbc6
|
chore: fix name
|
2021-01-27 16:26:34 -08:00 |
|
Leonardo de Moura
|
17edc1d615
|
test: inductive types for testing SizeOf.lean
|
2021-01-27 16:26:03 -08:00 |
|
Leonardo de Moura
|
992e0c5ded
|
feat: auxiliary sizeOf lemma recursor skeleton
TODO: minor premises
|
2021-01-27 16:18:53 -08:00 |
|
Leonardo de Moura
|
a0ed2d1738
|
chore: update tests
|
2021-01-27 15:17:51 -08:00 |
|
Leonardo de Moura
|
afdc19c2f1
|
feat: generalize indices at mkSizeOfAuxLemma
|
2021-01-27 15:16:43 -08:00 |
|
Leonardo de Moura
|
dff6bd300e
|
chore: add Expr.const?
|
2021-01-27 15:16:15 -08:00 |
|
Leonardo de Moura
|
8b3a28dd2b
|
test: reflection
|
2021-01-27 12:11:43 -08:00 |
|
Sebastian Ullrich
|
e5a9820830
|
chore: fix test
|
2021-01-27 15:04:59 +01:00 |
|
Sebastian Ullrich
|
d76378f12e
|
chore: fix pp.coercions description
@leodemoura still unsure about the ideal polarity of some pp options...
|
2021-01-27 14:46:37 +01:00 |
|
Sebastian Ullrich
|
7e521f0105
|
chore: remove remaining #lang lean4 in tests
|
2021-01-27 14:45:31 +01:00 |
|
Sebastian Ullrich
|
a3a8d76e96
|
chore: move pp_options.cpp to Lean
|
2021-01-27 14:16:12 +01:00 |
|
Sebastian Ullrich
|
c7347bbe0f
|
fix: that's not how Makefiles work
|
2021-01-27 12:34:48 +01:00 |
|
Leonardo de Moura
|
5f704b6b6f
|
chore: fix option name
|
2021-01-26 18:30:46 -08:00 |
|
Leonardo de Moura
|
5e3e37e7ed
|
chore: update stage0
|
2021-01-26 18:29:30 -08:00 |
|
Leonardo de Moura
|
6c119a1921
|
chore: use register_builtin_option
|
2021-01-26 18:24:56 -08:00 |
|
Leonardo de Moura
|
365a71ad9c
|
chore: remove dead options
|
2021-01-26 18:09:59 -08:00 |
|
Leonardo de Moura
|
4c3c049198
|
chore: use builtin_initialize
|
2021-01-26 18:09:45 -08:00 |
|
Leonardo de Moura
|
61f1fde40d
|
feat: add register_builtin_option keyword
|
2021-01-26 17:46:08 -08:00 |
|