2. Introduction and Definitions🔗

2.1. Introduction to Lean🔗

Comments are written with -- for single-line comments and /- ... -/ for block comments.

Function application in Lean is written with spaces. For example, write f x instead of f(x).

Type annotations use :. For example, write n : ℕ.

2.1.1. Useful input shortcuts🔗

x₀ is typed with x\_0
→ is \to
ℕ is \N
ℝ is \R
ε is \epsilon
∃ is \exists
∀ is \forall

2.2. Definitions🔗

Simple constant and function examples:

def hello := "Hello"

hello : String#check hello
"Hello"#eval hello

def add_one (n : Nat) : Nat :=
  n + 1

101#eval add_one 100

def add_one_lambda : Nat → Nat :=
  fun n => n + 1

101#eval add_one_lambda 100

Two-argument functions:

def maximum (n : Nat) (k : Nat) : Nat :=
  if n < k then
    k
  else
    n

333#eval maximum 80 333

def maximum_lambda : Int → Int → Int :=
  fun n k =>
    if n < k then k
    else n

333#eval maximum_lambda 80 333