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-11 15:46:54 -07:00
parent 7e380bf236
commit af1e670270
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
RELEASES.md
View file

@ -19,7 +19,7 @@ Unreleased
class GetElem (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) (Dom : outParam (Cont → Idx → Prop)) where
getElem (xs : Cont) (i : Idx) (h : Dom xs i) : Elem
```
The notation `a[i]` is not defined as follows
The notation `a[i]` is now defined as follows
```lean
macro:max x:term noWs "[" i:term "]" : term => `(getElem $x $i (by get_elem_tactic))
```