Sebastian Ullrich
6dfddbe2e7
feat: quotation precheck for choice nodes
2022-03-29 10:50:11 +02:00
Leonardo de Moura
a06cd40e29
feat: improve match expression support at simp
2022-03-28 17:17:01 -07:00
Leonardo de Moura
3c964f3b9f
feat: substitute auxiliary equations introduced by the split tactic
2022-03-28 14:29:28 -07:00
Leonardo de Moura
314bd3ae4c
fix: simpH? at match expression equation theorem generator
...
closes #1080
2022-03-28 12:48:54 -07:00
Leonardo de Moura
2dea5471da
feat: add support for HEq to the subst tactic
2022-03-28 12:23:55 -07:00
Leonardo de Moura
4801b37cfb
fix: exfalso
2022-03-27 14:56:24 -07:00
Sebastian Ullrich
4a9bc88a4e
chore: fix USE_GMP=OFF by removing GMP linking customization
2022-03-26 16:29:52 +01:00
Wojciech Nawrocki
96770b4d83
refactor: remove some code duplication
2022-03-26 06:26:41 -07:00
Wojciech Nawrocki
9223bf3640
feat: environment extension for RPC procedures
2022-03-26 06:26:41 -07:00
Leonardo de Moura
a2e467eb32
fix: mkEqnTypes
...
stop as soon as `lhs` and `rhs` are definitionally equal, and avoid
unnecessary case analysis.
This commit fixes the last issue exposed by #1074
fixes #1074
2022-03-25 19:13:21 -07:00
Leonardo de Moura
3a310fb122
fix: the eta for structures implementation in the elaborator was different from the implementation in the kernel
...
This issue was exposed by issue #1074
2022-03-25 18:24:15 -07:00
Leonardo de Moura
e53435979f
fix: remove hacky addAutoBoundImplicitsOld
2022-03-25 09:23:43 -07:00
Leonardo de Moura
6631d92d7b
fix: addAutoBoundImplicitsOld occurrences at MutualDef.lean and Structure.lean
...
This commit also fixes non-termination at `collectUnassignedMVars`
2022-03-25 09:07:59 -07:00
Leonardo de Moura
e48cc8901e
fix: add new addAutoBoundImplicits that avoids the hack at addAutoBoundImplicitsOld
2022-03-25 08:40:57 -07:00
Leonardo de Moura
519b780164
doc: document InfoTree issue
2022-03-25 07:12:07 -07:00
Leonardo de Moura
370e9c421f
fix: bug at deriving Hashable
2022-03-24 18:46:10 -07:00
E.W.Ayers
534aa88188
doc: MetaM
2022-03-24 16:57:42 -07:00
E.W.Ayers
1e69639fd2
doc: clarify mkLocalDecl
2022-03-24 14:59:46 -07:00
E.W.Ayers
6f5fc72c06
doc: Docstrings for LocalContext.lean
2022-03-24 14:59:46 -07:00
E.W.Ayers
24ebd78071
doc: Expr.lean
2022-03-24 14:52:09 -07:00
Wojciech Nawrocki
8f83c7ab32
feat: user-defined RPC handlers
2022-03-24 08:09:33 -07:00
Leonardo de Moura
fdbe893c40
fix: catch mkAppM exceptions
2022-03-23 17:35:04 -07:00
Leonardo de Moura
e0aa9fb290
chore: fix typo
2022-03-23 07:39:46 -07:00
Leonardo de Moura
2f67140603
fix: incorrect uses of getMVarType'
2022-03-22 14:11:29 -07:00
Leonardo de Moura
6007147d71
fix: allow universes to be postponed further
...
closes #1058
2022-03-22 13:57:58 -07:00
Leonardo de Moura
f3b181b972
chore: comment withoutPostponingUniverseConstraints
2022-03-22 13:57:58 -07:00
Mario Carneiro
c29da66c5a
fix: annotate binders in intro for hover / go to def
2022-03-22 12:10:51 +00:00
Sebastian Ullrich
c4d3c74837
feat: accept multiple patterns after matches
2022-03-21 17:59:02 +01:00
Sebastian Ullrich
faedfbe651
fix: antiquotation splices early in bootstrapping
2022-03-21 17:44:15 +01:00
Leonardo de Moura
3d9e587862
fix: check type mismatch at dependent pattern matching compiler
...
see issue #1057
2022-03-21 09:28:02 -07:00
Leonardo de Moura
321d6b0e67
feat: support for user-defined simp attributes in the simp tactic.
...
See `RELEASES.md`
TODO: make sure `-thm` also removes `thm` from user-defined simp attributes.
2022-03-20 18:45:57 -07:00
Leonardo de Moura
a2690d5278
feat: improve #eval command
2022-03-20 15:18:47 -07:00
Leonardo de Moura
6d926c7989
feat: macro expand match alternatives
...
see #371
This commit does not implement all features discussed in this issue.
It has implemented it as a macro expansion. Thus, the following is
accepted
```lean
inductive StrOrNum where
| S (s : String)
| I (i : Int)
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a | S a => toString a
```
It may confuse the Lean LSP server. The `a` on `toString` shows the
information for the first alternative after expansion (i.e., `a` is an `Int`).
After expansion, we have
```
def StrOrNum.asString (x : StrOrNum) :=
match x with
| I a => toString a
| S a => toString a
```
2022-03-20 14:20:13 -07:00
Leonardo de Moura
8f4d58893f
feat: update match parser
...
Support for
```
def fib (x : Nat) : Nat :=
match x with
| 0 | 1 => 1
| x+2 => fib (x+1) + fib x
```
TODO: expand `matchAlts`
2022-03-20 13:22:39 -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
Jakob von Raumer
a91f92c11e
feat: allow constants to be type classes
...
There no reason against constants to be type classes so it is just the check in `addClass` that is needed to be modified.
Closes #1054
2022-03-20 08:03:34 -07:00
Leonardo de Moura
1b357db3b0
fix: nasty bug at findDeclarationRangesCore?
...
We must search the environment extension first, and then the builtin
table. Otherwise, the builtin declarations do not change when we
modify the files.
closes #1021
2022-03-19 16:53:22 -07:00
Leonardo de Moura
ed7c8904a9
fix: propagate local and scope modifiers at elab_rules
...
closes #1039
2022-03-19 16:08:06 -07:00
Leonardo de Moura
82cd5c8eef
chore: cleanup
2022-03-19 15:52:04 -07:00
E.W.Ayers
da68f629f9
style: Apply.lean
...
Apply Leo's review requests.
2022-03-19 15:51:40 -07:00
E.W.Ayers
d954706fcf
feat: ApplyNewGoals config for apply
...
Lean.Meta.Tactic.apply now accepts an ApplyConfig argument.
`apply` now changes which metavariables are stored with choice
of the newGoals config.
This allows one to implement `fapply` and `eapply`.
An example of this is given in tests/lean/run/apply_tac.lean.
Closes #1045
2022-03-19 15:51:40 -07:00
Leonardo de Moura
c95d5f25a3
feat: convert ites into dites in the WF module
...
Motivation: the condition is often used in termination proofs.
2022-03-19 10:11:50 -07:00
Leonardo de Moura
36d955e8cc
feat: use simpler encoding for nonmutually recursive definitions
2022-03-19 09:43:18 -07:00
Leonardo de Moura
c7cdbf8ff8
feat: improve auto generated termination_by a bit
2022-03-19 09:28:19 -07:00
Leonardo de Moura
7dd38a7194
feat: add with_unfolding_all and rfl' tactics
2022-03-19 08:57:04 -07:00
Leonardo de Moura
fa74194638
fix: missing s.restore at expandTacticMacroFns
2022-03-19 08:34:54 -07:00
Leonardo de Moura
bd7827ed04
feat: dbg_trace tactic for low-level tactic debugging
2022-03-19 08:25:49 -07:00
Leonardo de Moura
a486503c62
chore: fold Nat literals at reduce
2022-03-18 17:10:46 -07:00
Leonardo de Moura
1514e39006
chore: add double ticks
2022-03-18 17:10:46 -07:00
Leonardo de Moura
42b707e250
perf: improve getMatchWithExtra
2022-03-18 17:10:46 -07:00
