Leonardo de Moura
16f7bef88f
chore: remove old frontend leftovers
2020-10-26 09:08:07 -07:00
Leonardo de Moura
95841490bb
chore: update stage0
2020-10-26 09:03:40 -07:00
Leonardo de Moura
deb283a415
chore: remove support for Lean3 scopes
2020-10-26 08:20:33 -07:00
Leonardo de Moura
e1c3c55027
chore: update stage0
2020-10-26 08:11:36 -07:00
Leonardo de Moura
bad6233389
chore: remove legacy support for modification objects
2020-10-26 08:10:51 -07:00
Leonardo de Moura
289ba6583c
chore: remove dead code
2020-10-26 07:58:15 -07:00
Leonardo de Moura
b4e8862716
chore: cleanup
2020-10-26 07:54:11 -07:00
Leonardo de Moura
cffa3b0039
chore: cleanup
2020-10-26 07:42:08 -07:00
Leonardo de Moura
e4b478ee6a
chore: remove support for quotations in the old frontend
2020-10-26 07:35:26 -07:00
Leonardo de Moura
7a24fe73ca
chore: remove dead code
2020-10-25 20:49:30 -07:00
Sebastian Ullrich
b856553b4f
chore: fix benchmark
2020-10-25 21:55:50 +01:00
Leonardo de Moura
b1b5460c4b
chore: update stage0
2020-10-25 10:23:03 -07:00
Leonardo de Moura
4838fb5c16
chore: remove source code for old frontend, equation compiler and tactics
2020-10-25 10:22:06 -07:00
Leonardo de Moura
94bc5ed7a3
chore: remove old frontend, equation compiler and tactics from build
2020-10-25 10:20:30 -07:00
Leonardo de Moura
e28b337a2c
chore: remove old frontend support from lean.cpp
...
We also remove the option `-n` (for new frontend)
2020-10-25 10:16:52 -07:00
Leonardo de Moura
2be41ad0ad
chore: update stage0
2020-10-25 10:00:43 -07:00
Leonardo de Moura
b80eab722b
chore: avoid hack at --deps
2020-10-25 10:00:05 -07:00
Leonardo de Moura
e3a982b0fa
chore: move update stage0
2020-10-25 09:54:08 -07:00
Leonardo de Moura
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -07:00
Leonardo de Moura
e67076ada8
chore: update stage0
2020-10-25 09:54:05 -07:00
Leonardo de Moura
98d0892910
chore: update test output
...
@Kha the test `Reformat.lean` is "almost" working. It produces some
reasonable output, but we get parser errors. I didn't investigate.
I am updated the test output just to make sure we don't get a failure
in the CI.
2020-10-25 09:54:05 -07:00
Leonardo de Moura
f89d34e0dc
chore: cleanup
2020-10-25 09:53:52 -07:00
Leonardo de Moura
8c6f536367
chore: avoid fun | ... => notation
...
@Kha the pretty printer fails when we use the `fun+match` macro. Example:
```
fun
| PSum.inl a => 1 + sizeof a
| PSum.inr b => 1 + sizeof b
```
The test `Reparen.lean` fails without this commit. Here is the error message
```
error: no known parenthesizer for kind 'Lean.Parser.Term.matchAlts'
```
2020-10-25 09:36:44 -07:00
Leonardo de Moura
eccf62946a
chore: update stage0
2020-10-25 09:20:07 -07:00
Leonardo de Moura
db9e390b4d
chore: remove new_frontend from tests
2020-10-25 09:16:38 -07:00
Leonardo de Moura
24a6ee1810
chore: use new frontend by default
2020-10-25 09:12:19 -07:00
Leonardo de Moura
fa101444b4
chore: fix tests
2020-10-25 09:11:13 -07:00
Leonardo de Moura
0554c75f48
chore: update stage0
2020-10-25 08:56:29 -07:00
Leonardo de Moura
1d338c4fc4
chore: move Core.lean to new frontend
2020-10-25 08:54:37 -07:00
Leonardo de Moura
5a130c6393
chore: update stage0
2020-10-25 05:50:58 -07:00
Leonardo de Moura
575db3bb3b
fix: improve structure/inductive commands universe level inference and validation
...
chore: cleanup
2020-10-25 05:46:51 -07:00
Leonardo de Moura
c4b9cc509c
fix: collect used universe levels in structure resulting type
2020-10-25 03:41:09 -07:00
Leonardo de Moura
9fe80411f9
chore: update stage0
2020-10-24 18:55:21 -07:00
Leonardo de Moura
3f0cc1d2ec
fix: library/constructions primitives crash at kernel_exception
2020-10-24 18:52:01 -07:00
Leonardo de Moura
609c54c57d
fix: allow structures to be in Prop
2020-10-24 16:57:57 -07:00
Leonardo de Moura
f7fcff56b8
chore: remove workaround
2020-10-24 16:48:43 -07:00
Leonardo de Moura
3ac752b413
chore: update stage0
2020-10-24 16:47:07 -07:00
Leonardo de Moura
9e181f5d91
fix: location parser
2020-10-24 16:46:30 -07:00
Leonardo de Moura
a4c69ec32c
chore: fix tests
2020-10-24 16:46:21 -07:00
Leonardo de Moura
ffa1647bd5
chore: move to new frontend
2020-10-24 16:42:10 -07:00
Leonardo de Moura
3941b55bb8
chore: remove old HasCoe
2020-10-24 16:22:52 -07:00
Leonardo de Moura
35f0bf7d77
chore: move to new frontend
2020-10-24 16:21:23 -07:00
Leonardo de Moura
72ec1833b3
chore: update stage0
2020-10-24 16:17:10 -07:00
Leonardo de Moura
632406adcd
fix: unused variables being included in theorems
2020-10-24 16:04:13 -07:00
Leonardo de Moura
fd9e9057c6
chore: update stage0
2020-10-24 15:55:36 -07:00
Leonardo de Moura
70bf755938
chore: cleanup
2020-10-24 14:15:56 -07:00
Leonardo de Moura
bb57e0f0b7
chore: update stage0
2020-10-24 13:30:02 -07:00
Leonardo de Moura
6ccf086b99
fix: modify mkAppM behavior and fix issue at Structural.lean
...
`Structural.lean` uses `mkAppM` for creating projections `PProd.fst`
and `PProd.snd`. However, given `x : (([Decidable p] → Bool) × Nat`,
the old ``mkApp `PProd.fst #[x]`` returned
```
Prod.fst ([Decidable p] → Bool) Nat x _inst
```
The extra unexpected argument `_inst` broke `Structural.lean`.
In the new implementation, it returns
```
Prod.fst ([Decidable p] → Bool) Nat x
```
which has type `[Decidable p] → Bool`.
2020-10-24 13:25:51 -07:00
Leonardo de Moura
e8c1647fa5
chore: improve condition
2020-10-24 12:37:11 -07:00
Leonardo de Moura
84926f62ea
chore: improve error message
2020-10-24 08:16:05 -07:00
