Leonardo de Moura
|
ae6a28af52
|
chore: remove unnecessary specialize
|
2021-06-28 10:11:23 -07:00 |
|
Leonardo de Moura
|
8f9fa8d04c
|
refactor: add BuiltinTactic.lean
|
2021-06-28 10:08:42 -07:00 |
|
Leonardo de Moura
|
712206f80e
|
refactor: add BindersUtil.lean
|
2021-06-28 08:44:16 -07:00 |
|
Leonardo de Moura
|
7e1bb3e65b
|
refactor: add MatchAltView.lean and PatternVar.lean
|
2021-06-28 08:29:47 -07:00 |
|
Leonardo de Moura
|
7f986c62ba
|
refactor: add Arg.lean
|
2021-06-28 08:10:16 -07:00 |
|
Leonardo de Moura
|
795b15581b
|
refactor: add BuiltinTerm.lean
|
2021-06-28 07:55:52 -07:00 |
|
Sebastian Ullrich
|
cef3ade164
|
fix: info on non-atomic simp args
|
2021-06-23 00:08:07 -07:00 |
|
Gabriel Ebner
|
3cff5ceb99
|
perf: make trace[...] ... notation lazy
|
2021-06-23 00:07:27 -07:00 |
|
Sebastian Ullrich
|
0948742da1
|
perf: fix formatting info tree unconditionally
|
2021-06-22 10:22:08 +02:00 |
|
Sebastian Ullrich
|
479edbe235
|
refactor: avoid unnecessary withLCtx
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
30a0954424
|
refactor: revert MonadRef changes
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
65f2874d86
|
chore: address reviews
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
eb1e285e26
|
chore: style
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
91e3100e30
|
fix: properly resolve syntax kinds in macro/elab_rules
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
3f4ab0a2af
|
feat: implement elab_rules
TODO: infer category from quotation type
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
a86efc4796
|
fix: info tree context of command macros
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
9101c9d5da
|
feat: support docstrings on syntax/macro/...
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
652097e184
|
fix: separate ElabInfo from MacroExpansionInfo, always emit the former before the latter
This way all hover info is contained in the former info node kinds
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
459e2e8cea
|
chore: print info tree elaborators
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
da4c46370d
|
feat: store elaborator declaration name in info tree
|
2021-06-21 10:17:26 -07:00 |
|
Sebastian Ullrich
|
062cc5d567
|
chore: remove inline
|
2021-06-19 15:01:43 +02:00 |
|
Sebastian Ullrich
|
720954d63a
|
perf: Lean.Elab.Do: avoid code explosion
|
2021-06-17 12:51:23 -07:00 |
|
Sebastian Ullrich
|
b4e9ba1500
|
perf: specialize more monad instances
|
2021-06-17 11:25:58 +02:00 |
|
Sebastian Ullrich
|
380c6c285a
|
perf: specialize some monad instances
|
2021-06-17 11:25:58 +02:00 |
|
Leonardo de Moura
|
f816e6107b
|
fix: report (pending) type mismatch errors in simp arguments
|
2021-06-16 11:35:49 -10:00 |
|
Sebastian Ullrich
|
884aa03584
|
fix: implement overlooked have syntax
|
2021-06-15 17:46:16 +02:00 |
|
Daniel Selsam
|
ded51882a0
|
feat: pp motives and misc delab fixes
|
2021-06-13 00:06:27 +02:00 |
|
Sebastian Ullrich
|
cc2f483951
|
chore: note on previous commit
|
2021-06-10 18:25:39 +02:00 |
|
Sebastian Ullrich
|
e4bf5977d9
|
fix: syntax pattern match against multiple identifiers
|
2021-06-10 18:15:40 +02:00 |
|
Gabriel Ebner
|
960cfd9cae
|
feat: store expected type in info tree
|
2021-06-07 16:23:22 -07:00 |
|
Daniel Fabian
|
63d58c2f64
|
refactor: use Except instead of Option in the JSON code.
|
2021-06-07 12:10:10 +02:00 |
|
Daniel Fabian
|
825218cd4a
|
feat: use Except instead of Option in the JSON deriving handlers.
|
2021-06-07 12:10:10 +02:00 |
|
Daniel Fabian
|
9200de01ef
|
refactor: fix code review comments.
|
2021-06-06 06:40:09 -07:00 |
|
Daniel Fabian
|
968ae18f20
|
fix: deal with params for inductive predicates.
|
2021-06-06 06:40:09 -07:00 |
|
Daniel Fabian
|
4e53b3bdbf
|
fix: use motive from brecOn in structural recursion for predicates.
|
2021-06-06 06:40:09 -07:00 |
|
Daniel Fabian
|
822c551aa2
|
test: Add a bunch of test for structural recursion on predicates.
|
2021-06-06 06:40:09 -07:00 |
|
Daniel Fabian
|
ec6f7d9bd6
|
feat: Implement structural recursion for inductive predicates.
|
2021-06-06 06:40:09 -07:00 |
|
Sebastian Ullrich
|
b82b90a687
|
feat: KeyedDeclAttribute: expose declaration names
|
2021-06-06 15:32:58 +02:00 |
|
Daniel Fabian
|
4b7cb058d3
|
feat: Add support for inductive types to FromJson and ToJson handlers.
|
2021-06-05 13:53:10 +02:00 |
|
Daniel Fabian
|
06d1d3ae07
|
fix: Use UInt64 in deriving handler for Hashable.
|
2021-06-03 06:38:44 -07:00 |
|
Leonardo de Moura
|
37da993032
|
chore: remove HashableUSize instances
|
2021-06-02 08:48:11 -07:00 |
|
Leonardo de Moura
|
43812444a7
|
chore: Hashable => HashableUSize
|
2021-06-02 07:24:26 -07:00 |
|
Leonardo de Moura
|
96b5574f21
|
fix: use withoutProofIrrelevance at getFixedPrefix
|
2021-05-27 13:42:22 -07:00 |
|
Sebastian Ullrich
|
e918e39ed0
|
feat: have: remove unnecessary whitespace check and allow name- and type-less have
|
2021-05-25 14:25:14 +02:00 |
|
Leonardo de Moura
|
8b4cdcfddd
|
chore: fix mutable variable shadowing
|
2021-05-22 19:24:41 -07:00 |
|
Leonardo de Moura
|
b91e22af2b
|
fix: fixes #241
|
2021-05-22 19:10:07 -07:00 |
|
Leonardo de Moura
|
af4485f40e
|
fix: fixes #482
|
2021-05-21 19:20:24 -07:00 |
|
Leonardo de Moura
|
8eceb07caf
|
feat: new discriminant refinement procedure
|
2021-05-21 18:08:11 -07:00 |
|
Sebastian Ullrich
|
93327e2324
|
fix: tactic state on {/·
|
2021-05-21 17:13:33 -07:00 |
|
Leonardo de Moura
|
73797841ba
|
feat: add findDiscrRefinementPath
The new method is going to be used to improve the discriminant
refinement procedure.
|
2021-05-20 21:54:48 -07:00 |
|