Sebastian Ullrich
43c875fd7a
fix: tactic block indentation
2020-10-27 14:09:33 +01:00
Leonardo de Moura
c979d81934
refactor: add polymorphic methods for updating/querying reducibility status
2020-10-26 17:07:28 -07:00
Leonardo de Moura
bddc826648
chore: remove unnecessary liftMs
2020-10-26 16:27:45 -07:00
Leonardo de Moura
79609938a8
feat: allow universe constraints to be postponed longer
...
Before this commit, each `isDefEq u v` invocation would fail if there
were pending universe level constraints. This commit, moves the
postponed universe constraints back to the `MetaM` state.
It also adds the combinator
```lean
withoutPostponingUniverseConstraints x
```
which executes `x` and throws an error if there are pending universe
constraints. We use the combinator at `elabApp` and `elabBinders`.
Without this commit, we would fail to elaborate simple terms such as
```lean
Functor.map Prod.fst (x s)
```
because after elaborating `Prod.fst` and trying to ensure its type
match the expected one, we would be stuck at the universe constraint:
```
u =?= max u ?v
```
Another benefit of the new approach is better error messages. Instead
of getting a mysterious type mismatch constraint, we get a list of
universe contraints the system is stuck at.
cc @Kha
2020-10-26 15:50:05 -07:00
Leonardo de Moura
5481999560
chore: cleanup
2020-10-26 14:25:38 -07:00
Leonardo de Moura
91d51d06e0
chore: cleanup
2020-10-26 14:00:13 -07:00
Leonardo de Moura
40f99327e9
fix: missing withMainMVarContext
2020-10-26 11:35:54 -07:00
Leonardo de Moura
c55a65fe00
chore: cleanup
2020-10-26 10:58:56 -07:00
Leonardo de Moura
7e244686e9
chore: remove old notation
2020-10-26 09:16:51 -07:00
Leonardo de Moura
16f7bef88f
chore: remove old frontend leftovers
2020-10-26 09:08:07 -07:00
Leonardo de Moura
deb283a415
chore: remove support for Lean3 scopes
2020-10-26 08:20:33 -07:00
Leonardo de Moura
bad6233389
chore: remove legacy support for modification objects
2020-10-26 08:10:51 -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
13c2a8ff51
chore: remove #lang lean4 header
2020-10-25 09:54:07 -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
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
9e181f5d91
fix: location parser
2020-10-24 16:46:30 -07:00
Leonardo de Moura
632406adcd
fix: unused variables being included in theorems
2020-10-24 16:04:13 -07:00
Leonardo de Moura
70bf755938
chore: cleanup
2020-10-24 14:15:56 -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
Leonardo de Moura
01251a56e0
chore: improve error message
2020-10-24 07:57:02 -07:00
Leonardo de Moura
d89f559683
chore: fix definitions
...
See commit before update stage0 for explanation.
2020-10-24 07:27:25 -07:00
Leonardo de Moura
0af4b6fb6f
chore: remove hack that produces big search space
2020-10-24 07:21:06 -07:00
Leonardo de Moura
525fb7ca91
chore: cleanup
2020-10-24 06:26:32 -07:00
Leonardo de Moura
0ab38742db
chore: cleanup
2020-10-24 06:18:01 -07:00
Leonardo de Moura
78c05e8f46
chore: move to new frontend
2020-10-23 16:13:55 -07:00
Leonardo de Moura
3de97ddc27
feat: run linters in the new frontend
2020-10-23 14:04:28 -07:00
Leonardo de Moura
21757b2be9
feat: add helper option for fixing bootstrapping issue at src/Init/Data/Int/Basic
2020-10-23 11:13:04 -07:00
Leonardo de Moura
de66ca3943
feat: add helper functions for writing macros
2020-10-23 10:59:59 -07:00
Leonardo de Moura
bebd5075fd
chore: cleanup
2020-10-23 10:00:23 -07:00
Leonardo de Moura
c7dc61adb9
chore: cleanup
2020-10-23 10:00:23 -07:00
Sebastian Ullrich
2ea5d7e480
fix: build
2020-10-23 18:55:06 +02:00
Sebastian Ullrich
fc5f93331d
feat: profile new frontend
2020-10-23 18:34:47 +02:00
Sebastian Ullrich
0720334450
feat: make profileit actually usable
2020-10-23 18:34:47 +02:00
Leonardo de Moura
8c03075e58
feat: improve function expected error message
2020-10-23 06:52:51 -07:00
Leonardo de Moura
f339efa100
feat: improve invalid named argument error message
2020-10-23 06:47:07 -07:00
Leonardo de Moura
1e8a4d1da5
chore: avoid useless failed to synthesize CoeFun ... tail message
2020-10-23 06:15:29 -07:00
Leonardo de Moura
14e3b26e57
fix: missing instantiateMVars
2020-10-23 05:38:08 -07:00
Leonardo de Moura
de4bede6ff
fix: use correct metavar context
2020-10-23 05:15:36 -07:00
Leonardo de Moura
d4a67baa8e
refactor: rename MonadFinally.finally' => MonadFinally.tryFinally'
2020-10-22 17:40:30 -07:00
Leonardo de Moura
02521397ac
refactor: rename MonadExceptOf.catch => MonadExceptOf.tryCatch
2020-10-22 17:27:15 -07:00
Leonardo de Moura
a37e2ae46f
refactor: simplify MonadFunctor
2020-10-22 17:05:34 -07:00
Leonardo de Moura
fa3c32d3b1
chore: remove adaptExcept
2020-10-22 16:56:23 -07:00
Leonardo de Moura
bc8b78f481
chore: cleanup
2020-10-22 16:30:06 -07:00
