From 00a8b5b605b5bbee814312fe52a8fd601f266c32 Mon Sep 17 00:00:00 2001 From: Pranshu Sharma Date: Tue, 20 May 2025 21:11:57 +1000 Subject: [PATCH] Main intro file --- intro.lean | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 intro.lean diff --git a/intro.lean b/intro.lean new file mode 100644 index 0000000..986b735 --- /dev/null +++ b/intro.lean @@ -0,0 +1,16 @@ + + +def hello : String := "Hello" + +def add1 (n : Nat) : Nat := n + 1 + +def maximum (n : Nat) (k : Nat) : Nat := + if n < k then + k + else n + +def PStr : Type := String + +def OnePlusOneIsTwo : Prop := 1 + 1 = 2 + +theorem onePlusOneIsTwo : OnePlusOneIsTwo := rfl