max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
26905 commits 1 branch 0 tags 5.3 GiB
Commit graph

7279 commits

Author SHA1 Message Date
Sebastian Ullrich
312944e784 fix: hover etc. on complex declaration name 2022-01-19 12:27:03 +01:00
Leonardo de Moura
1e21815e41 fix: equality theorem generation when named patterns are used 
closed #945
 2022-01-18 14:37:51 -08:00
Leonardo de Moura
1c1e6d79a7 feat: add equality proof for named patterns 
The user can optionally name the equality proof.
The new test demostrates how to name the equality proof.

closes #501
 2022-01-18 12:43:01 -08:00
Leonardo de Moura
cd903bde77 refactor: [s : Setoid α] => {s : Setoid α} or (s : Setoid α) 
See comment at https://github.com/leanprover/lean4/issues/952#issuecomment-1015265136

cc @gebner
 2022-01-18 09:24:06 -08:00
Leonardo de Moura
b266961068 chore: fix test 2022-01-17 17:24:09 -08:00
Leonardo de Moura
2a17233f1c chore: fix test 2022-01-17 17:07:08 -08:00
Leonardo de Moura
de11f7e1bc feat: add sizeOf spec lemmas as simp theorems 2022-01-17 16:14:38 -08:00
Gabriel Ebner
ab276a5ae3 chore: show declaration with sorry in #eval 2022-01-17 13:18:22 -08:00
Leonardo de Moura
dd3d8f6fad feat: complete namespaces 
closes #940
 2022-01-17 10:03:36 -08:00
Leonardo de Moura
da06bb6605 fix: matching inside new termination_by 2022-01-17 08:47:05 -08:00
Leonardo de Moura
189f4bd372 chore: fix tests 2022-01-15 12:18:09 -08:00
Leonardo de Moura
c1fccf19cb chore: fix test 2022-01-15 11:46:11 -08:00
Leonardo de Moura
b0d9c16c7a chore: rename PointedType => NonemptyType 2022-01-15 11:43:53 -08:00
Henrik Böving
c1b31a57eb feat: store ModuleData of imported modules in EnvironmentHeader 2022-01-15 10:40:52 -08:00
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