Leonardo de Moura
2a9ba9f795
fix: add support for hierachical names containing numerical parts
...
closes #677
2021-09-17 19:21:49 -07:00
Leonardo de Moura
a823ebdbe0
chore: make it clear how it is being parsed
...
We are planning to change the `<|>` precedence here.
2021-09-16 13:41:01 -07:00
Leonardo de Moura
0a898965a3
chore: use snake_case for user-facing tactic names
2021-09-16 10:23:12 -07:00
Leonardo de Moura
c2a5e37c60
feat: simp discharger
2021-09-16 10:11:27 -07:00
Sebastian Ullrich
08c2c31fcd
feat: IO.FS.removeDir(All)
2021-09-16 07:01:37 -07:00
Daniel Selsam
8d370f151f
fix: space before 'at' in location
2021-09-15 18:41:26 +02:00
Leonardo de Moura
6fb2a2b47b
chore: remove ≅ notation for HEq
...
We don't really needed it here.
2021-09-15 08:06:32 -07:00
Leonardo de Moura
d2240a99e5
feat: add erw tactic back as a macro
2021-09-12 19:29:12 -07:00
Leonardo de Moura
42436254ee
fix: code
2021-09-12 19:11:21 -07:00
Leonardo de Moura
bfa1c86b24
feat: add optional config parser to rewrite tactics
2021-09-12 19:05:15 -07:00
Leonardo de Moura
ea37c64b52
feat: add Meta.Rewrite.Config
2021-09-12 18:44:08 -07:00
Leonardo de Moura
71229f45fb
chore: "upgrate" to doc string
2021-09-12 18:30:08 -07:00
Leonardo de Moura
8c82302aca
refactor: add config syntax and macro for boilerplate code
2021-09-12 18:09:19 -07:00
Leonardo de Moura
218b9c87b0
feat: expose APIs for creating IO.Error objects
2021-09-11 17:14:43 -07:00
Leonardo de Moura
4630c9af7c
feat: add congruence lemmas for let-expressions
2021-09-10 18:53:23 -07:00
Leonardo de Moura
1576040c87
chore: remove workaround
2021-09-09 19:30:31 -07:00
Leonardo de Moura
f5a4b30d5f
fix: broken proof
2021-09-09 18:11:05 -07:00
Leonardo de Moura
5154f462f8
feat: add reduce conv tactic
2021-09-09 17:47:10 -07:00
Leonardo de Moura
496cc92ae9
feat: add simpMatch helper conv tactic
2021-09-09 17:29:32 -07:00
Leonardo de Moura
b5b5370181
feat: add delta to conv mode
2021-09-09 13:07:33 -07:00
Leonardo de Moura
4087525cba
feat: add delta tactic
2021-09-09 13:07:33 -07:00
Leonardo de Moura
9032ddd773
chore: add simp lemma for converting Nat.add back into + notation
2021-09-08 14:58:13 -07:00
Leonardo de Moura
716ffecf89
chore: add sorry tactic
2021-09-08 08:10:37 -07:00
Leonardo de Moura
12af1480d6
feat: add specialize tactic
2021-09-08 08:00:02 -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
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
3714cf16ec
refactor: lazy evaluation for <|>
...
see #617
2021-09-07 17:06:10 -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
ab63382158
feat: add helper functions for optimized noConfusion
2021-09-06 10:33:34 -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
53a3831fd5
feat: add apply conv macro
2021-09-03 20:23:15 -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
44e7033c27
feat: add support for forall_congr at conv
2021-09-03 16:57:15 -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
Leonardo de Moura
397774157f
feat: nested tactic support in conv mode
2021-09-02 19:12:05 -07:00
Leonardo de Moura
41ce24e2c6
feat: add done and traceState conv tactics
2021-09-02 18:46:03 -07:00
Leonardo de Moura
33361929b9
feat: add rewrite conv tactic
2021-09-02 18:13:19 -07:00
Leonardo de Moura
a8b434f93d
feat: add missing parsers
2021-09-02 15:25:34 -07:00
Leonardo de Moura
9bb5d4dc93
chore: Nat.ltWf => Nat.lt_wf
2021-09-02 07:51:41 -07:00
Leonardo de Moura
f1c5e7596b
chore: fix build
2021-09-01 19:26:56 -07:00
Leonardo de Moura
e3ccc03a45
chore: add nested conv tactics
2021-09-01 18:44:35 -07:00
Leonardo de Moura
254f82c273
feat: basic infrastructure for conv mode
2021-09-01 17:00:45 -07:00
Leonardo de Moura
6d8058034a
chore: basic conv mode parsers
2021-09-01 15:35:32 -07:00
Leonardo de Moura
8fec444e55
feat: add injections tactic
2021-08-31 19:12:06 -07:00
Leonardo de Moura
ad539a23e1
chore: cleanup proofs for tutorial
2021-08-31 16:37:40 -07:00
Leonardo de Moura
c491f829e0
feat: elaborator for the calc notation
...
- It produces better error messages.
- It tweaks the elaboration order.
- It adds a checkpoint after each step.
- It avoids the `show .. from ..` workaround.
2021-08-31 09:56:49 -07:00
Leonardo de Moura
b500a2053d
feat: split tactic for splitting match and if terms
2021-08-30 18:31:20 -07:00
Leonardo de Moura
ad3b0b4a2c
feat: nary generalize tactic
...
This commit also fixes a bug when using multiple targets with the
`induction` and `cases` tactics.
2021-08-30 16:31:39 -07:00
