Leonardo de Moura
|
13a3215d0d
|
chore: use Subarray combinators
|
2020-10-28 19:52:59 -07:00 |
|
Leonardo de Moura
|
131cb7036f
|
feat: add combinators for Subarray
|
2020-10-28 19:49:38 -07:00 |
|
Leonardo de Moura
|
4ba21ea10c
|
chore: cleanup src/Array/Basic.lean
|
2020-10-28 19:35:42 -07:00 |
|
Leonardo de Moura
|
d87b8b876f
|
chore: add temporary workaround
cc @Kha
|
2020-10-28 16:57:46 -07:00 |
|
Leonardo de Moura
|
6765440724
|
chore: remove clutter
|
2020-10-28 14:11:06 -07:00 |
|
Leonardo de Moura
|
88fb6acae3
|
chore: remove clutter
|
2020-10-28 13:29:17 -07:00 |
|
Leonardo de Moura
|
3e6b2964cf
|
chore: minor cleanup
|
2020-10-28 13:18:45 -07:00 |
|
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 |
|