Chris Lovett
bc3900cbb9
doc: small fixes
2021-09-07 19:19:58 -07:00
Leonardo de Moura
3fc226dc6d
chore: fix tests
2021-09-07 19:14:30 -07:00
Leonardo de Moura
445cc3085f
refactor: avoid Name, MVarId, and FVarId confusion
2021-09-07 19:06:50 -07:00
Leonardo de Moura
750c2507da
test: add *> laziness test
...
This commit also fixes a broken test
Closes #617
The following operators are now lazy: `<|>`, `>>`, `*>`, `<*`, `<*>`
2021-09-07 18:03:15 -07:00
Leonardo de Moura
e5600b03df
chore: update stage0
2021-09-07 17:51:26 -07:00
Leonardo de Moura
53ec43ff9b
refactor: lazy evaluation for >>, <*>, <*, and *>
...
see issue: #617
2021-09-07 17:50:34 -07:00
Leonardo de Moura
51b7c4cf21
chore: remove Nondet.lean
...
It was too "unsafe", and it is dead code.
2021-09-07 17:36:20 -07:00
Leonardo de Moura
6ea7869c6a
chore: "fix" <|> notation declaration
...
The `infix` declaration was generating a delaborator, but it is
producing the invalid term
```
ConstantFunction.f myFun 3 <|> fun _ => ConstantFunction.f myFun 4
```
It is invalid because the `macro_rules` for `<|>` is based on
`binop_lazy%` which introduces the `fun _ =>` for us.
I tried to use
```
notation:20 a:21 " <|> " b:20 => HOrElse.hOrElse a fun _ : Unit => b
```
but the delaborator generator does not work for this case.
2021-09-07 17:29:27 -07:00
Leonardo de Moura
eb94e87195
chore: fix some tests
2021-09-07 17:20:21 -07:00
Leonardo de Moura
c5f9113dcf
test: use <|> at binop_lazy test
2021-09-07 17:10:36 -07:00
Leonardo de Moura
2f0a936f88
chore: update stage0
2021-09-07 17:08:16 -07:00
Leonardo de Moura
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -07:00
Leonardo de Moura
3b136816fe
chore: update stage0
2021-09-07 13:39:59 -07:00
Leonardo de Moura
55f01fb6e1
feat: elaborate binop_lazy%
2021-09-07 13:30:09 -07:00
Leonardo de Moura
61976c4e56
chore: update stage0
2021-09-07 13:29:50 -07:00
Leonardo de Moura
d991c20859
chore: add binop_lazy%
...
This is a gadget for issue #617 .
2021-09-07 13:00:36 -07:00
Leonardo de Moura
5a862a06c6
chore: remove leftover
2021-09-07 12:57:27 -07:00
Leonardo de Moura
f46eedac84
fix: fixes #655
2021-09-07 12:17:28 -07:00
Leonardo de Moura
a8007ee827
chore: update stage0
2021-09-07 08:26:55 -07:00
Leonardo de Moura
c8406a301d
chore: reduce src/include/lean
2021-09-07 08:24:54 -07:00
Leonardo de Moura
c93982d10c
chore: disable pp.analyze for now
...
see #651
2021-09-07 07:51:43 -07:00
Leonardo de Moura
ebd8f1efa7
chore: avoid object.h dependencies
2021-09-07 07:31:48 -07:00
Daniel Selsam
b36baa143f
feat: improved name-unresolving in delab
...
Fixes #641
2021-09-07 16:26:00 +02:00
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
