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

6417 commits

Author SHA1 Message Date
Leonardo de Moura
656b7a8d87 chore: fix tests 2021-03-11 10:51:11 -08:00
Leonardo de Moura
8188789cf4 chore: fix test 2021-03-11 10:16:37 -08:00
Leonardo de Moura
35b2f596f1 test: use decide and nativeDecide 
They are not active yet.
 2021-03-11 07:46:33 -08:00
Leonardo de Moura
48b855bfe5 chore: fix tests 2021-03-10 18:45:22 -08:00
Leonardo de Moura
55157a3108 chore: fix test 2021-03-10 14:51:24 -08:00
Leonardo de Moura
1ea4bdb9cd fix: add "band-aid" for #341 
closes #341

This is another instance of a compiler bug.
It is in the code that is still written in C/C++.
We need to infer types in the compiler, and we reused the kernel type
checker for this.
However, the compiler performs transformations that may produce type
incorrect terms.
This happens in code that makes heavy use of dependent types (like the
new test).
This is just a workaround for this particular instance of the problem.
The definitive solution will only happen when we replace
this part of the compiler with Lean code, and implement a custom
`inferType` method for the compiler.
 2021-03-10 08:11:41 -08:00
Sebastian Ullrich
b6622d2bef feat: server: preserve full range of messages 2021-03-10 17:09:41 +01:00
Leonardo de Moura
0ea267e4de feat: add simp lemma preprocessor 2021-03-09 19:16:14 -08:00
Leonardo de Moura
0068732751 test: benchmarks for simp 2021-03-09 15:09:51 -08:00
Leonardo de Moura
4c82f5c688 test: perf experiments 2021-03-09 13:42:47 -08:00
Leonardo de Moura
0c29987a82 chore: clenaup test 2021-03-08 18:19:15 -08:00
Leonardo de Moura
90cab68332 feat: keep going if there are missing alternatives at induction/cases 2021-03-08 17:09:53 -08:00
Leonardo de Moura
ef4ab9c1d1 fix: report error if too many variable names have been provided at induction/cases alternative 2021-03-08 16:26:53 -08:00
Leonardo de Moura
4bbcd305b5 fix: disable implicit-lambdas when elaborating patterns 
@Kha, Jason's example on issue #337 suggests that injecting
implicit-lambdas while elaborating patterns is problematic.
The elaborator was injecting `fun {Γ} =>` before the
pattern variable `ftm`.
So, I disabled the implicit-lambda during pattern elaboration. I
didn't find an example where it would be useful.

see #337

cc @JasonGross
 2021-03-08 15:45:30 -08:00
Leonardo de Moura
f321ad213f fix: reset set of stuck mvars after reporting they are stuck 
This bug produced the doubled error message at issue #337
 2021-03-08 12:46:50 -08:00
Leonardo de Moura
5d3f0606d2 feat: include type of type in "mismatch errors" 
@Kha we do that in Lean 3. It helps when the error is due to incorrect universe levels.

BTW, I had to update `tests/lean/server/content_diag.json` since the
error message is different, but a few other stuff changed too.
Could you please take a look whether the test is still correct?
 2021-03-08 09:30:34 -08:00
Leonardo de Moura
0e3aa2c29b fix: scope of forallTelescopeReducing 
Nested constructors were being processed using an extended local context.
Fix issue reported by @JasonGross at Zulip.

closes #338
 2021-03-08 08:29:48 -08:00
Leonardo de Moura
4bbf498004 chore: fix tests 2021-03-07 18:52:46 -08:00
Leonardo de Moura
9901898258 feat: add Nat.gcd 
This commit also fix some theorem names to new naming convention.
 2021-03-07 18:47:02 -08:00
Leonardo de Moura
0a881315ba feat: optional preprocessing tactic at induction and cases 
cc @Kha
 2021-03-07 14:50:49 -08:00
Leonardo de Moura
5ba171d946 test: for Int.negSucc bug 2021-03-07 13:09:23 -08:00
Leonardo de Moura
51e7f45af2 refactor: cases 
remove dead `induction/cases` code
 2021-03-07 12:37:02 -08:00
Leonardo de Moura
19899d087e refactor: induction 2021-03-07 12:04:36 -08:00
Jan Hrcek
2753822fe7
doc: fix typos 2021-03-07 15:06:02 +01:00
Leonardo de Moura
6ec5c1de54 chore: fix test 
`set_option` command after `by` tactic block is ambiguous.
We need to indent or use `{ ... }`.

cc @Kha
 2021-03-06 16:46:18 -08:00
Leonardo de Moura
061b9bf60f feat: set_option in terms and tactics 
closes #330
 2021-03-06 16:43:10 -08:00
Leonardo de Moura
0ed3f08c1b feat: open in terms and tatics 
See #330
 2021-03-06 15:33:00 -08:00
Leonardo de Moura
7a79ef62d1 fix: bug at hasSyntheticSorry 
It was missing a constructor, and not taking assigned metavariables
into account.

Fixes a problem reported by @JasonGross at Zulip
 2021-03-05 19:08:10 -08:00
Leonardo de Moura
9b02a80416 fix: fixes #335 2021-03-05 18:16:49 -08:00
Leonardo de Moura
fc79b794ba fix: missing error messages 
Issue reported by @JasonGross
 2021-03-05 17:20:04 -08:00
Leonardo de Moura
be4cf605fd feat: improve error message 
closes #331
 2021-03-05 13:42:54 -08:00
Leonardo de Moura
5e9ccf19d7 fix: fixes #329 2021-03-05 13:42:54 -08:00
Leonardo de Moura
e228ca38b8 test: add set example 2021-03-04 19:16:12 -08:00
Leonardo de Moura
66f1a88f2c feat: simp [-decl] 2021-03-04 17:50:44 -08:00
Leonardo de Moura
b26c7087fe chore: increase test size 2021-03-04 17:27:24 -08:00
Joe Hendrix
9bd60c7519 feat: Nat/Fin/UInt instances of bitwise classes 2021-03-04 15:42:43 -08:00
Leonardo de Moura
2b78de650a test: experiment 2021-03-04 14:48:49 -08:00
Leonardo de Moura
30287836b0 test: OfNatSound 2021-03-04 13:48:01 -08:00
Leonardo de Moura
1fedbfb9a3 feat: simp only 2021-03-04 11:58:34 -08:00
Leonardo de Moura
960e964b71 feat: allow user to "erase" [simp] lemmas 2021-03-04 11:36:12 -08:00
Leonardo de Moura
130a087ecf feat: Lean 3 french single quote notation 2021-03-04 09:43:59 -08:00
Leonardo de Moura
3107473c9f feat: add rename tactic 
cc @Kha
 2021-03-03 18:32:25 -08:00
Leonardo de Moura
1ecc50f809 test: contradiction 2021-03-03 17:13:25 -08:00
Leonardo de Moura
6cdc6cb1d0 feat: add contradiction 2021-03-03 17:00:54 -08:00
Leonardo de Moura
4aec7579db test: add do equivalence examples 2021-03-03 13:44:30 -08:00
Leonardo de Moura
f1245f9dc7 fix: bug at isDefEqOffset 
fixes #326
 2021-03-02 17:28:40 -08:00
Leonardo de Moura
5626b537c7 chore: move nondet to Std/Control/Nondet.lean 2021-03-02 07:57:25 -08:00
Leonardo de Moura
533731d61e chore: fix nondet 2021-03-02 07:38:44 -08:00
Leonardo de Moura
769e3a9082 chore: fix test 2021-02-28 16:38:04 -08:00
Leonardo de Moura
140cdbe942 test: tactic framework 2021-02-26 19:34:55 -08:00