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

5604 commits

Author SHA1 Message Date
Leonardo de Moura
1ce80d5ba7 feat: hide auxiliary declarations 2020-09-15 16:50:16 -07:00
Leonardo de Moura
19a7927f10 feat: sanitizeNames 
@Kha I am using `_shadowed.<idx>` suffix for marking variables that
have been shadowed. It is a bit verbose, but at least it is easy to
understand understand error messages such as
```
shadow.lean:4:0: error: type mismatch
  h
has type
  x._shadowed.1 = x._shadowed.1
but it is expected to have type
  x = x
```
It is better than the old cryptic version
```
shadow.lean:4:0: error: type mismatch
  h
has type
  x = x
but it is expected to have type
  x = x
```
 2020-09-15 16:28:50 -07:00
Leonardo de Moura
4e99b19a96 fix: expandMatchDiscr cannot be a macro 
The `matchType` created by the macro is bad for dependent pattern
matching. The `tst8` and `tst9` at `matchTac` failed to be elaborated
when using the macro.
 2020-09-15 13:29:28 -07:00
Leonardo de Moura
75814c2d21 chore: fix tests 2020-09-15 11:11:05 -07:00
Leonardo de Moura
3ebecc8caa test: open and export 2020-09-15 10:46:40 -07:00
Sebastian Ullrich
1e6faf3f28 test: ignore \r when diffing 2020-09-15 09:32:00 -07:00
Sebastian Ullrich
897f277a3e test: strip mvar suffixes 2020-09-15 09:32:00 -07:00
Leonardo de Moura
b8d90d77db feat: macro scope as the single mechanism for creating fresh names 
cc @Kha
 2020-09-14 20:09:07 -07:00
Leonardo de Moura
fde43e071d feat: improve matchType inference 2020-09-14 19:44:45 -07:00
Leonardo de Moura
cc3b48ce16 fix: check inductive datatype parameters in constructor resulting type 2020-09-14 16:56:13 -07:00
Leonardo de Moura
634f063631 feat: finish commit "using indentation" 2020-09-14 16:40:52 -07:00
Leonardo de Moura
ca90ff8b59 test: have-by in tactic mode 
@Kha By adding `have-by` macro (in term mode), we got `have-by` in
tactic mode without writing a single line of code :)
 2020-09-14 15:17:25 -07:00
Leonardo de Moura
a6b19cd4af feat: expand show-by and have-by macros 2020-09-14 15:08:28 -07:00
Leonardo de Moura
fc4ab139b5 feat: indented by 
@Kha This one is not as useful as the indented `do`. When writing
interactive proofs I like the error message at the `}` showing the
resulting tactic state. We can simulate it using a `skip` in the end of the sequence :)
We remove the `skip` when the proof is done. Note that, the last `;`
is usually not part of the `by`. Example:
```lean
theorem ex (x y z : Nat) : y = z → y = x → x = z :=
fun _ _ =>
  have x = y by apply Eq.symm; assumption; -- <<< the last `;` is part of the `have`
  Eq.trans this (by assumption)
```
 2020-09-14 14:20:02 -07:00
Leonardo de Moura
4c6a589e6c feat: indented do blocks 
@Kha it is soooooo much nicer :)
 2020-09-14 13:44:51 -07:00
Leonardo de Moura
163b0a7a3f fix: protected 
- `protected` outside of a namespace is an error.
- Fix `protected` in recursive definitions.

cc @Kha
 2020-09-14 13:09:04 -07:00
Leonardo de Moura
7c0216595e fix: remove duplicate error messages due to variable(s) 
In Lean4, we re-elaborate `variable`(s) for each command, but we don't
want the error messages due to `variable` to appear in the log
multiple times.
 2020-09-14 12:44:25 -07:00
Sebastian Ullrich
a93a53b4b5 feat: more IO Task functions 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
77cbaa752c fix: Task: make reference and -j0 semantics eager, simplify 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
5b83ceb1b5 feat: IO.mapTask, IO.bindTask 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
307a833798 feat: implement IO.asTask as primitive using always-run tasks 2020-09-14 17:57:33 +02:00
Sebastian Ullrich
c672bd657f feat: IO.asTask 2020-09-14 17:57:33 +02:00
Leonardo de Moura
c58252ad74 chore: move more tests to new frontend 2020-09-13 16:13:20 -07:00
Leonardo de Moura
5da7f0b50b fix: set constApprox := false at SynthInstance 
We don't want contraints such as
```
?m a =?= Nat
```
to be solved as
```
?m := fun a => Nat
```
durint type class resolution.
 2020-09-13 16:11:27 -07:00
Leonardo de Moura
21c8366645 chore: fix test output 2020-09-13 13:50:00 -07:00
Leonardo de Moura
2ee1821f13 fix: ensure expectedType at fun body 2020-09-13 13:44:05 -07:00
Leonardo de Moura
32e26799ed chore: move more tests to new frontend 2020-09-13 13:28:12 -07:00
Leonardo de Moura
498d7886eb chore: fix test output 2020-09-13 13:21:58 -07:00
Leonardo de Moura
7b90f7d956 fix: synthesize pending mvars before trying coercions to Fun 
`tests/lean/repr_issue.lean` cannot be elaborated with this modification.
 2020-09-13 13:19:05 -07:00
Leonardo de Moura
d936b9461f fix: always ensure expectedType when processing overloaded symbols and/or notation 2020-09-13 11:59:13 -07:00
Leonardo de Moura
c080d42692 chore: move tests to new frontend 2020-09-13 10:16:15 -07:00
Leonardo de Moura
897289599a fix: ignore auxiliary declarations at subst and assumption 2020-09-13 09:59:37 -07:00
Leonardo de Moura
ac6fd1382d fix: collectDeps issue 2020-09-13 09:47:00 -07:00
Leonardo de Moura
e181c1adee refactor: add DefEqM 
The idea is to make clear that the field `posponed` is transient
state. It is only used during `isDefEq`.
The refactoring was motivated by a bug I found where the `posponed`
constraints were not being handled correctly. For example,
the `check (e : Expr)` method was returning `true`, but leaving pending
universe constraints at `postponed`.

cc @Kha
 2020-09-12 16:42:16 -07:00
Leonardo de Moura
0967ad7e91 feat: extend/cleanup isLevelDefEqAux 
`tests/lean/run/toExpr.lean` could not be processed by the new
frontend without these extensions.
 2020-09-12 15:38:48 -07:00
Leonardo de Moura
ab44cd28f1 chore: move more tests to new frontend 2020-09-12 09:04:39 -07:00
Leonardo de Moura
e1e65e83da fix: try to synthesize instance for substructures 2020-09-12 08:58:13 -07:00
Leonardo de Moura
a784005729 chore: move more tests to new frontend 2020-09-12 07:54:12 -07:00
Leonardo de Moura
09244c73f4 fix: lval resolution 2020-09-12 07:45:36 -07:00
Leonardo de Moura
cc520d422c fix: ensure no unassigned mvars at #eval 2020-09-12 07:18:43 -07:00
Leonardo de Moura
f242a958fc chore: move more tests to new frontend 2020-09-11 17:36:37 -07:00
Leonardo de Moura
a8de3c5115 fix: isDefEq configuration in the elaborator 2020-09-11 17:36:28 -07:00
Leonardo de Moura
bbc3bec53b chore: move more tests to new frontend 2020-09-11 16:28:57 -07:00
Leonardo de Moura
bf703c9cab fix: bug at inductive datatype resulting universe inference 2020-09-11 16:07:22 -07:00
Leonardo de Moura
b02cda0408 chore: move more tests to new frontend 2020-09-11 15:31:14 -07:00
Leonardo de Moura
2c2a357f28 chore: remove disabled test 2020-09-11 15:05:00 -07:00
Leonardo de Moura
151012cb39 feat: remove emptyc elaboration hack 
@Kha I removed the hack. We know get a nice error message.
 2020-09-11 14:41:44 -07:00
Leonardo de Moura
ff9b562e66 chore: move test 2020-09-11 14:40:21 -07:00
Leonardo de Moura
cc6104b369 fix: bug in the old frontend 
It had to be fixed because we have code that needs to be compiled with
the old frontend, and the hacks we used to workaround this issue are
incompatible with the new frontend.
 2020-09-11 14:12:03 -07:00
Leonardo de Moura
7950413526 feat: improve choice nodes + postpone 2020-09-11 12:45:38 -07:00