Leonardo de Moura
e3241e82bc
feat: define PointedType as { α : Type u // Nonempty α }
2022-01-14 20:36:51 -08:00
Leonardo de Moura
a438a2ee21
feat: elaborate arbitrary_or_ofNonempty% and use it to define constants
2022-01-14 17:22:39 -08:00
Leonardo de Moura
c34adb7dd5
feat: allow partial definitions to be define if type is non empty
2022-01-14 16:50:36 -08:00
Joscha
6d809e7cd1
test: remove references test
...
This test no longer works since the 'references' request now requires at
least a watchdog, but this kind of test only work with file workers.
2022-01-14 09:18:57 +01:00
Sebastian Ullrich
37f5be1b26
chore: fix servertest_init_exit
2022-01-14 09:18:57 +01:00
Leonardo de Moura
6d235586f0
fix: ignore TC failures while processing patterns
...
closes #948
2022-01-13 10:55:09 -08:00
Leonardo de Moura
1620987b6c
fix: recursive applications in discriminants
2022-01-13 09:56:33 -08:00
Leonardo de Moura
8c45c844aa
test: add wellfounded test
2022-01-12 17:16:43 -08:00
Leonardo de Moura
3fbf5acbee
fix: add missing [reducible] annotations Init/WF.lean
2022-01-12 17:12:55 -08:00
Leonardo de Moura
98864f707e
test: add test for #879
...
The new `termination_by` syntax should address issue #879
closes #879
2022-01-12 16:25:09 -08:00
Leonardo de Moura
9162901c86
fix: expandTerminationByNonCore
2022-01-12 16:22:54 -08:00
Leonardo de Moura
91a0ac8a12
feat: elaborate new termination_by syntax
2022-01-12 16:15:30 -08:00
Leonardo de Moura
addcbc6fa3
feat: process termination_by syntax
2022-01-12 16:15:30 -08:00
Leonardo de Moura
111d09fda3
fix: must apply afterCompilation attributes *after* smart unfolding definition was declared
...
The `[simp]` attribute checks whether the smart unfolding defintion
has been declared.
closes #946
2022-01-12 08:28:03 -08:00
Leonardo de Moura
45bd328d5e
fix: tests and add WellFoundedRelation.rel to list of definitions to unfold at decreasing_tactic
2022-01-12 08:28:03 -08:00
Gabriel Ebner
50abc3e295
fix: correctly pretty-print @Eq
2022-01-12 09:41:41 +01:00
Leonardo de Moura
4e5a51aa24
chore: fix test
2022-01-11 16:23:26 -08:00
Leonardo de Moura
068cc700d8
test: ackermann
2022-01-11 15:03:07 -08:00
Leonardo de Moura
381f66428a
chore: use termination_by'
...
We are going to define a higher level syntax for `termination_by`.
2022-01-11 15:00:53 -08:00
Leonardo de Moura
d953ac8d0d
feat: allow users to use initialize registerBuiltinDerivingHandler ...
2022-01-11 09:50:09 -08:00
Leonardo de Moura
762b0f42ba
chore: fix tests
2022-01-10 15:06:03 -08:00
Leonardo de Moura
4c918a2363
feat: use default_decreasing_tactic at WF/Fix.lean
2022-01-10 14:55:38 -08:00
Leonardo de Moura
739ef7d166
fix: annotate let rec declarations as auxDecl
...
Reason:
1- Tactics such as `assumption` should ignore them.
2- We must annotate recursive applications with `mkRecAppWithSyntax`.
2022-01-10 14:35:05 -08:00
Leonardo de Moura
57b8912279
chore: fix tests
2022-01-10 14:33:02 -08:00
Leonardo de Moura
0dd3ce0598
chore: fix test
2022-01-10 14:31:23 -08:00
Leonardo de Moura
929aafa4c8
fix: generate an error if declaration name clashes with variable name
...
closes #799
2022-01-10 12:08:11 -08:00
Leonardo de Moura
b2d26380f2
fix: remove auxiliary discriminant let-declarations
2022-01-07 15:03:19 -08:00
Leonardo de Moura
1cf8467847
feat: add unfold conv tactic
2022-01-07 13:51:45 -08:00
Leonardo de Moura
49d0f3af52
test: unfold tactic
2022-01-07 13:51:45 -08:00
Leonardo de Moura
b797c982fc
feat: add mkUnfoldProof
2022-01-07 13:51:45 -08:00
Gabriel Ebner
f146d456ce
fix: only enable InsertReplaceEdit if supported
2022-01-07 20:28:10 +01:00
larsk21
8c2d7a35d3
fix: make set_option completion replace typed partial name
2022-01-07 17:06:26 +01:00
Mario Carneiro
dcaf3c615f
fix: induction generalizing precedence
2022-01-07 10:45:45 +01:00
Leonardo de Moura
bef161caf7
feat: add better support for discharging equation theorem hypotheses
2022-01-06 14:42:23 -08:00
Leonardo de Moura
90b179bea9
fix: add equation theorems even if definition supports smart unfolding
...
See new test.
2022-01-06 13:53:03 -08:00
Leonardo de Moura
d8d7d63830
fix: registers eqns info before adding definition
...
Otherwise `[simp]` at definition will fail to generate equational theorems.
2022-01-06 12:24:40 -08:00
Leonardo de Moura
7acbbb4fbb
fix: auxiliary whnfAux used at mkEqns
2022-01-06 09:57:41 -08:00
Leonardo de Moura
60934bf1d5
feat: add support for removing [simp] attribute from definitions with equational theorems
2022-01-05 16:57:59 -08:00
Leonardo de Moura
c2e52bd577
feat: use getEqnsFor? when applying [simp] at definitions
2022-01-05 15:59:39 -08:00
Leonardo de Moura
030e932db8
feat: use getEqnsFor? at simp
2022-01-05 11:28:24 -08:00
Leonardo de Moura
4d1343d670
chore: use _eq instead of eq to name auto generated equational theorems
2022-01-04 17:23:34 -08:00
Leonardo de Moura
b2918e0c76
test: add tests for WF.mkEqns
2022-01-04 17:18:51 -08:00
Leonardo de Moura
d782a97f5c
feat: add WF.mkProof for WF.mkEqns
2022-01-04 17:00:54 -08:00
Sebastian Ullrich
64971a1e3c
fix: term macro errors should be fatal
2022-01-04 11:20:18 +01:00
Leonardo de Moura
b9f7d1defb
fix: constant folding after erasure
...
closes #909
2022-01-03 10:33:07 -08:00
Leonardo de Moura
52b6a04088
test: for #916
2022-01-03 07:57:16 -08:00
Gabriel Ebner
e605c541d0
fix: do not infer type in erase_irrelevant
...
At the time erase_irrelevant is called, we have already eliminated the
`cast`-applications. Therefore non-atomic expressions may no longer
be well-typed (and `infer_type` can fail).
2022-01-03 07:13:55 -08:00
Sebastian Ullrich
555584375a
fix: compare fields top-down in deriving Ord
2022-01-03 07:02:13 -08:00
Henrik Böving
2d85c9ba2f
chore: fix notation test
...
The ppNotationCode.lean test failed because the output of the notation
elaborator changed (purposely), adapt it to the new output.
2022-01-03 13:47:11 +01:00
Gabriel Ebner
70ef4e529c
feat: allow attributes on structures and inductives
2021-12-23 08:04:36 -08:00
