Henrik Böving
b46aa05241
doc: new way to install lean4-mode
...
The current installation procedure requires you to have and update a checkout
of lean4 yourself which is rather annoying if you are just someone who
wants to work with lean4-mode for another project. straight.el +
use-package provide a nice alternative to the current approach.
2021-09-07 16:23:18 +02:00
Henrik Böving
4eca7c2a39
fix: add lsp-mode to the lean4-mode dependencies
...
lean4-mode implicitly relies on lsp-mode being installed, however this
dependency is not explicitly declared. The version used is the latest
release version which seemed to work out for me.
2021-09-07 16:23:18 +02:00
Leonardo de Moura
e2cc056cdd
fix: assertion violation
2021-09-07 07:16:12 -07:00
Leonardo de Moura
d643dfd1c7
chore: update stage0
2021-09-06 12:02:41 -07:00
Leonardo de Moura
70f2200778
chore: remove enum command
...
Now, `inductive` is also efficient for big enumeration types
2021-09-06 12:01:37 -07:00
Leonardo de Moura
1ce2ff394c
chore: update stage0
2021-09-06 11:57:21 -07:00
Leonardo de Moura
d174ffb075
chore: update stage0
2021-09-06 11:55:51 -07:00
Leonardo de Moura
a7c621854e
feat: optimized noConfusion for enumeration types
2021-09-06 11:52:36 -07:00
Leonardo de Moura
d43a1c7d9a
chore: move Constructions to Meta
2021-09-06 10:51:11 -07:00
Leonardo de Moura
ab63382158
feat: add helper functions for optimized noConfusion
2021-09-06 10:33:34 -07:00
Leonardo de Moura
09326df213
chore: fix test output
2021-09-06 07:39:57 -07:00
Leonardo de Moura
ec30a6b7e8
chore: update stage0
2021-09-06 07:37:16 -07:00
Leonardo de Moura
1d68f38aa6
feat: use approxDepth to compute hash code
2021-09-06 07:36:41 -07:00
Leonardo de Moura
5ce97286bb
chore: update stage0
2021-09-06 07:28:10 -07:00
Leonardo de Moura
fa29428934
feat: use 8-bits to store the approximate depth on an expression
...
We are going to use this information to (try to) minimize the number
of hash collisions.
2021-09-06 07:26:51 -07:00
Leonardo de Moura
65509c5617
doc: add basic perf documentation
2021-09-06 07:12:36 -07:00
Leonardo de Moura
20022f3c6d
chore: update stage0
2021-09-05 20:44:08 -07:00
Leonardo de Moura
a8044eb252
feat: improve Match module for patterns containing Fin and UInt literals
2021-09-05 20:43:40 -07:00
Leonardo de Moura
fc334ffbee
fix: pattern matching on UInt
2021-09-05 19:15:59 -07:00
Leonardo de Moura
0d751f3bd3
chore: update stage0
2021-09-05 18:49:02 -07:00
Leonardo de Moura
dc3b4a06f3
fix: missing case
2021-09-05 18:43:39 -07:00
Leonardo de Moura
fa94ce0660
chore: fix test output
2021-09-05 17:49:03 -07:00
Leonardo de Moura
da31ea4b5b
chore: update stage0
2021-09-05 17:17:30 -07:00
Leonardo de Moura
6f075e6ece
feat: add enum command for declaring enumeration types
...
closes #654
2021-09-05 16:58:49 -07:00
Leonardo de Moura
e4410cfbf8
chore: missing Fin instances
2021-09-05 16:09:18 -07:00
Leonardo de Moura
c3bb948009
feat: ignore nested proofs in patterns
2021-09-05 15:46:03 -07:00
Leonardo de Moura
029c5b74a2
feat: ignore implicit arguments at congr conv tactic
2021-09-05 09:44:52 -07:00
Leonardo de Moura
d3c487ddbf
feat: change lhs and rhs conv tactic semantics
...
They can now be applied to non binary applications.
2021-09-05 09:29:40 -07:00
Wojciech Nawrocki
b6971e4733
fix: don't crash watchdog on notifications to closed files
2021-09-04 18:50:27 -07:00
Leonardo de Moura
ef8aadcbea
fix: fixes #653
2021-09-04 18:42:33 -07:00
Leonardo de Moura
aedc706e7d
feat: in modifier at conv tactic
...
It is just a macro for `pattern`
2021-09-04 18:20:33 -07:00
Leonardo de Moura
41cfef5bc4
feat: add pattern conv tactic
2021-09-04 18:02:46 -07:00
Leonardo de Moura
53a3831fd5
feat: add apply conv macro
2021-09-03 20:23:15 -07:00
Leonardo de Moura
94bc386fb4
feat: remark goals as conv goals at the end of nested tactic block
2021-09-03 19:52:51 -07:00
Leonardo de Moura
de455a9010
chore: add tactic' => ... which preserves the conv goal annotation
2021-09-03 19:41:39 -07:00
Leonardo de Moura
6988560177
feat: apply allGoals (try rfl) at end of conv nested blocks
2021-09-03 19:21:34 -07:00
Leonardo de Moura
bfefeb6e5a
chore: use compact structure instance notation
2021-09-03 18:59:26 -07:00
Leonardo de Moura
229373a7e6
chore: fix test
2021-09-03 18:59:13 -07:00
Leonardo de Moura
e6c9da0fcc
feat: add support for implication at congr conv tactic
2021-09-03 18:50:19 -07:00
Leonardo de Moura
69075c775f
fix: missing withMainContext
2021-09-03 16:57:24 -07:00
Leonardo de Moura
44e7033c27
feat: add support for forall_congr at conv
2021-09-03 16:57:15 -07:00
Leonardo de Moura
3f70bc543f
feat: add simp conv tactic
2021-09-03 12:06:29 -07:00
Leonardo de Moura
75b8d9aa86
feat: add support for classes with a prefix of outParams at deriving ...
2021-09-03 11:33:09 -07:00
Leonardo de Moura
bbb74bfd9a
feat: elaborate optional deriving after def
2021-09-03 10:22:17 -07:00
Leonardo de Moura
d682d60025
chore: cleanup
2021-09-03 09:48:36 -07:00
Leonardo de Moura
8a268e184b
feat: update def parser with optional deriving ...
2021-09-03 09:42:17 -07:00
Leonardo de Moura
35c0cc3c91
feat: deriving support for type aliases
2021-09-03 09:33:01 -07:00
Leonardo de Moura
8a249bddd2
feat: add try rfl at end of convTarget
2021-09-03 08:14:47 -07:00
Leonardo de Moura
18bcc458d0
feat: add 'enter' conv tactic macro
2021-09-03 08:11:37 -07:00
Leonardo de Moura
b5b5ef6fdf
feat: add funext conv tactic
2021-09-03 08:00:37 -07:00
