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

chore: missing code block annotation

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-10 17:08:54 -08:00
parent 1b5e9c7c83
commit 002412e9d0
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

@ -155,7 +155,7 @@ inductive HasType : {n : Nat} → Fin n → Vector Ty n → Ty → Type where
```
* Eliminate auxiliary type annotations (e.g, `autoParam` and `optParam`) from recursor minor premises and projection declarations. Consider the following example
```
```lean
structure A :=
x : Nat
h : x = 1 := by trivial