max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: fix typo

Browse source
This commit is contained in:
Leonardo de Moura 2022-07-10 10:15:23 -07:00
parent 351fc6ea04
commit fd0e9e1c52
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASES.md
View file

@ -61,7 +61,7 @@ Unreleased
example (a : Array Int) (i : USize) (h : i.toNat < a.size) : Int :=
a[i] -- Ok
```
The `get_tactic_tactic` is defined as
The `get_elem_tactic` is defined as
```lean
macro "get_elem_tactic" : tactic =>
`(first
@ -69,7 +69,7 @@ Unreleased
| fail "failed to prove index is valid, ..."
)
```
The `get_elem_tactic_trivial` auxiliary tactic can be extended by using `macro_rules`. By default, it tries `trivial`, `simp_arith`, and a special case for `Fin`. In the future, it will also try `linarith`.
The `get_elem_tactic_trivial` auxiliary tactic can be extended using `macro_rules`. By default, it tries `trivial`, `simp_arith`, and a special case for `Fin`. In the future, it will also try `linarith`.
You can extend `get_elem_tactic_trivial` using `my_tactic` as follows
```lean
macro_rules