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

6360 commits

Author SHA1 Message Date
Leonardo de Moura
0615020cf7 feat: make sure Expr.approxDepth does not overflow 2022-01-22 07:45:19 -08:00
Leonardo de Moura
79dec8fa7c chore: fix test 2022-01-20 17:19:29 -08:00
Leonardo de Moura
d39025e343 test: add test for issue #951 2022-01-20 17:16:06 -08:00
Leonardo de Moura
0c959b6942 chore: fix tests 2022-01-20 15:25:59 -08:00
Leonardo de Moura
f9fa24435d chore: remove problematic instance hasOfNatOfCoe 
See #403
See https://github.com/leanprover-community/mathport/issues/94
 2022-01-20 14:47:25 -08:00
Leonardo de Moura
b1a92f5cbf feat: better Repr instances for Level.Data and Expr.Data 
see #619
 2022-01-20 09:45:30 -08:00
Leonardo de Moura
ff4be1e1db feat: add Repr instances for Level and Expr 
closes #619

TODO: a better `Repr` instance for `Expr.Data`
 2022-01-20 09:26:06 -08:00
Leonardo de Moura
d190d6dda4 fix: use default reducibility when proving equation theorems for definition 
Addresses issue reported by @fpfu at #945
 2022-01-20 08:23:51 -08:00
Leonardo de Moura
f5509ab867 fix: equational lemma generation for definitions using named patterns 
closes #945
 2022-01-19 17:45:54 -08:00
Sebastian Ullrich
bbec84bb18 chore: more output on trace.Elab.info 2022-01-19 21:40:29 +01:00
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
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
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