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

16258 commits

Author SHA1 Message Date
Leonardo de Moura
327717ade8 chore: add leading_parser and trailing_parser notation 
It will replace `parser!` and `tparser!`
 2021-03-11 09:08:35 -08:00
Leonardo de Moura
9f88ea8047 chore: remove old decide!, nativeRefl!, and nativeDecide! 2021-03-11 08:06:20 -08:00
Leonardo de Moura
babdde9068 chore: activate decide and nativeDecide 2021-03-11 07:54:54 -08:00
Leonardo de Moura
90c5f35702 refactor: implement decide and nativeDecide as tactics 
TODO: update stage0 and activate
 2021-03-11 07:50:54 -08:00
Sebastian Ullrich
7b9f9e806f feat: Syntax.topDown 2021-03-11 13:22:18 +01:00
Leonardo de Moura
68143ca8ba chore: trace[...]! ==> trace[...] 
@Kha I think this one is a good change, there is no real reason for
using the `!` suffix here.
 2021-03-10 18:44:43 -08:00
Leonardo de Moura
30ba56126b fix: missing case 
Lean should not get stuck at universe constraints such as `?u =?= ?u + 1`.
 2021-03-10 14:48:02 -08:00
Leonardo de Moura
a3923eecc8 feat: filter duplicate universe constraints at error message 2021-03-10 14:40:25 -08:00
Leonardo de Moura
847f95021a fix: losing postponed universe constraints 
This bug was exposed by #342
 2021-03-10 14:18:03 -08:00
Leonardo de Moura
904c23e901 chore: add annotations 
We need these extra annotations after we fix a bug a `commitWhen`.
In the `commitWhen` bug, we were "losing" postponed constraints.
 2021-03-10 14:11:03 -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
Sebastian Ullrich
c2f7ecaf37 feat: server: also transmit array of goals 2021-03-10 17:09:41 +01:00
Leonardo de Moura
8f580a5a70 refactor: remove SimpLemmaKind 2021-03-09 19:25:02 -08:00
Leonardo de Moura
0ea267e4de feat: add simp lemma preprocessor 2021-03-09 19:16:14 -08:00
Leonardo de Moura
2004ea5ec0 feat: add AuxLemma.lean 2021-03-09 18:25:19 -08:00
Leonardo de Moura
23319da6c0 fix: position info for rw tactics of the form rw [h1, h2, ..] 2021-03-08 18:18:37 -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
142d6cbcbc chore: truncate error messages endPos 
@Kha, @Vtec234, @mhuisi:
This is a bit hackish, but it improves the usuability quite a bit in
VS Code. Without this hack, I often get huge blocks of "red squiggly lines".
 2021-03-08 16:44:33 -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
a4abdbf277 refactor: add checkApp 
Add comment describing possible extension.
 2021-03-08 15:26:07 -08:00
Leonardo de Moura
0c4d72c1d5 refactor: add implicitLambda argument 2021-03-08 15:21:32 -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
a7ac27b0e8 refactor: use mutual recursion 2021-03-08 07:41:58 -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
8afa96d6c8 fix: incorrect lean_dec, lean_nat_to_int consumes the argument 2021-03-07 12:57:58 -08:00
Leonardo de Moura
51e7f45af2 refactor: cases 
remove dead `induction/cases` code
 2021-03-07 12:37:02 -08:00
Leonardo de Moura
e5f1bd2eb9 chore: fix Core.lean 2021-03-07 12:08:37 -08:00
Leonardo de Moura
55115a4a1b feat: add inferInstance tactic 2021-03-07 12:08:25 -08:00
Leonardo de Moura
19899d087e refactor: induction 2021-03-07 12:04:36 -08:00
Leonardo de Moura
5f5cc55d6a feat: add helper method 2021-03-07 12:04:14 -08:00
Leonardo de Moura
dfa5cf9282 chore: add optional preprocessing tactic 2021-03-07 12:03:54 -08:00
Leonardo de Moura
1e13c26de3 chore: prepare to change inductionAlts 2021-03-07 10:22:27 -08:00
Leonardo de Moura
08fc25217d chore: cleanup, fix docs 2021-03-07 09:01:54 -08:00
Leonardo de Moura
b7019d913e chore: remove unnecessary lifts and implicits 
Use autobound and autolift features
 2021-03-07 09:01:54 -08:00
Leonardo de Moura
6d236fbf2e chore: fix docstring 2021-03-07 09:01:54 -08:00
Jan Hrcek
2753822fe7
doc: fix typos 2021-03-07 15:06:02 +01: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
b3d83aa199 feat: set_option parser for terms and tactics 2021-03-06 15:38:02 -08:00
Leonardo de Moura
ad68c5cbaa refactor: polymorphic elabSetOption 2021-03-06 15:33:01 -08:00
Leonardo de Moura
4a39201d55 fix: ambiguity 
```
def f (x : Nat) : IO Unit := do
IO.println x

open Nat in
def g (x : Nat) := succ x
```

cc @Kha
 2021-03-06 15:33:00 -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
4bcfc5f9a6 feat: open parser for terms and tactics 2021-03-06 15:32:59 -08:00
Leonardo de Moura
8249620c9e refactor: add polymorphic elabOpenDecl method 2021-03-06 15:32:59 -08:00
Leonardo de Moura
d75c4e2101 chore: cleanup 2021-03-06 15:32:59 -08:00
Leonardo de Moura
b6c388780f chore: cleanup 2021-03-06 15:32:59 -08:00