natural-number-game

Solututions to the Natural Number Game

git clone: git://git.pablopie.xyz/natural-number-game
Log
Files
Refs
README

Commit: 0c28dc75738c5d23a2b89c98e9328abe07de34f1
Parent: fbeeea210094f75c6500e09da94d7339ab623b20
Author: Pablo <pablo-escobar@riseup.net>
Date: Thu, 30 Dec 2021 23:55:18 +0000

Renamed the mynat type to ℕ

Diffstat

3 files changed, 3 insertions, 11 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	advanced-addition.lean	3	2	1
Modified	function.lean	2	1	1
Modified	preposition.lean	9	0	9

diff --git a/advanced-addition.lean b/advanced-addition.lean
@@ -4,7 +4,8 @@ begin
   exact hs,
 end
 
-theorem succ_succ_inj {a b : mynat} (h : succ(succ(a)) = succ(succ(b))) :  a = b := 
+theorem succ_succ_inj {a b : mynat} 
+                      (h : succ(succ(a)) = succ(succ(b))) : a = b := 
 begin
   apply succ_inj,
   apply succ_inj,

diff --git a/function.lean b/function.lean
@@ -3,7 +3,7 @@ begin
   exact h(p),
 end
 
-example : mynat → mynat :=
+example : ℕ → ℕ :=
 begin
   intro n,
   exact 3 * n + 2,

diff --git a/preposition.lean b/preposition.lean
@@ -66,12 +66,3 @@ begin
   cc,
 end
 
-
-
-
-
-
-
-
-
-