16 lines
258 B
Text
16 lines
258 B
Text
|
|
|
|
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
|