Leonardo de Moura
86cb5cbdfe
chore: remove auxiliary definition for old frontend
2020-10-28 09:46:38 -07:00
Leonardo de Moura
de568b1268
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
852bd66542
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
227faa0aad
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
c2b2f62bc4
chore: remove dead code
2020-10-28 09:33:19 -07:00
Leonardo de Moura
c59f673f60
chore: cleanup
2020-10-28 09:33:19 -07:00
Leonardo de Moura
465a0d3970
chore: cleanup
2020-10-28 09:33:19 -07:00
Leonardo de Moura
ffc5ccf118
chore: remove dead code
2020-10-28 09:33:19 -07:00
Sebastian Ullrich
8f01619c3d
perf: work around parser performance issue I forgot about and the speedcenter had to remind me of
2020-10-28 10:11:45 +01:00
Leonardo de Moura
01f8bcfc87
chore: remove dead code
2020-10-27 19:23:14 -07:00
Leonardo de Moura
898a08a0c1
chore: avoid Has prefix in type classes
...
closes #203
2020-10-27 18:29:19 -07:00
Leonardo de Moura
97c93ec557
chore: prepare to rename
2020-10-27 18:09:03 -07:00
Leonardo de Moura
1fba699b2c
chore: remove unused names
2020-10-27 16:28:19 -07:00
Leonardo de Moura
ff493751b5
chore: HasFormat ==> ToFormat
2020-10-27 16:19:14 -07:00
Leonardo de Moura
5fed774461
chore: HasRepr ==> Repr
2020-10-27 16:15:10 -07:00
Leonardo de Moura
10c32fcf94
chore: HasToString => ToString
2020-10-27 16:11:48 -07:00
Leonardo de Moura
5ea49c92bb
chore: cleanup
2020-10-27 13:26:21 -07:00
Leonardo de Moura
592b73daf6
feat: expand suffices macro
2020-10-27 13:05:13 -07:00
Leonardo de Moura
d6418299c7
chore: naming convention
2020-10-27 13:05:13 -07:00
Leonardo de Moura
9d82b965b3
feat: allow by ... at suffices
2020-10-27 13:05:13 -07:00
Leonardo de Moura
573ca7dcad
chore: remove workarounds
2020-10-27 13:05:13 -07:00
Leonardo de Moura
ec28b26233
chore: improve StateRefT notation
2020-10-27 13:05:12 -07:00
Leonardo de Moura
633578cfaf
chore: use StateRefT macro
2020-10-27 13:05:12 -07:00
Leonardo de Moura
f80e2c1db6
feat: elaborate StateRefT macro
2020-10-27 13:05:12 -07:00
Leonardo de Moura
828c0b832f
chore: add StateRefT macro
2020-10-27 13:05:12 -07:00
Sebastian Ullrich
8e16589f60
fix: reimplement import profiler
2020-10-27 18:53:22 +01:00
Sebastian Ullrich
b1f49637c2
fix: re-enable --profile by passing the startup options via the global ios
...
@leodemoura We should probably reimplement `profileit` in pure Lean when we want to get rid of `io_state`
2020-10-27 18:51:35 +01:00
Leonardo de Moura
270f6df5cb
chore: remove aux_match module
...
This is not needed anymore since the old equation compiler was removed.
2020-10-27 09:51:55 -07:00
Leonardo de Moura
7d8c079d71
chore: remove abstract_context_cache
2020-10-27 09:37:21 -07:00
Leonardo de Moura
95acb5cf3a
chore: remove old fun_info module
2020-10-27 09:37:21 -07:00
Leonardo de Moura
c841f83c04
chore: remove dead code
2020-10-27 09:37:21 -07:00
Leonardo de Moura
503504e962
chore: cleanup
2020-10-27 09:37:21 -07:00
Leonardo de Moura
16710581ad
chore: remove dead code
2020-10-27 09:37:21 -07:00
Sebastian Ullrich
bc1acf7a9f
doc: document orelse restriction for the pretty printer
2020-10-27 17:29:57 +01:00
Sebastian Ullrich
7696f71518
Revert "chore: avoid fun | ... => notation"
...
This reverts commit 8c6f536367
2020-10-27 16:50:58 +01:00
Sebastian Ullrich
78a8bc7b7e
feat: adapt elaborator to preceding change
2020-10-27 16:50:58 +01:00
Sebastian Ullrich
d8a1742d57
feat: introduce suppressInsideQuot
2020-10-27 16:50:58 +01:00
Sebastian Ullrich
912d24a3ee
fix: disambiguate fun syntax alternatives to help the pretty printer
2020-10-27 16:48:31 +01:00
Sebastian Ullrich
20ed65605b
fix: don't parenthesize juxtaposed tactics
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
84692acd0e
fix: do not introduce parentheses implied by indentation
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
c0e117daa4
fix: Option.ToMessageData
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
5f67c359bc
chore: simplify formatter token separation logic
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
73323a7500
fix: remove obsolete workaround confusing the formatter
...
We don't generate antiquotations for `tparser!` anymore
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
33c861a80e
fix: parenthesizer: really make sure a trailing parser is of the same category as the continuation
2020-10-27 14:09:33 +01:00
Sebastian Ullrich
eb125c52f1
fix: never pretty-print whitespace before checkNoWsBefore
2020-10-27 14:09:33 +01:00
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
