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

fix: doc

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-23 09:41:42 -08:00
parent 74686a149a
commit caa3136558
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
doc/lean3changes.md
View file

@ -25,7 +25,9 @@ def Prod.str : Nat × Nat → String :=
fun (a, b) => "(" ++ toString a ++ ", " ++ toString b ++ ")"
structure Point where
x y z : Nat
x : Nat
y : Nat
z : Nat
def Point.addX : Point → Point → Nat :=
fun { x := a, .. } { x := b, .. } => a+b