Syntax & Notation

1-- Infix form (what you normally write)
2#eval 2 + 3     -- 5
3
4-- Prefix form (same thing!)
5#eval HAdd.hAdd 2 3  -- 5
6
7-- This works for all operators
8#eval 10 - 3         -- 7
9#eval HSub.hSub 10 3 -- 7
10
11-- Comparison operators too
12#eval 5 > 3          -- true
13#eval GT.gt 5 3      -- true
14
15-- You can use parentheses to make precedence explicit
16#check (2 + 3) * 4   -- Nat

1-- Function arrows
2#check Nat → Nat       -- Unicode arrow (\to)
3#check Nat -> Nat      -- ASCII arrow
4
5-- Universal quantifier
6#check ∀ n : Nat, n = n   -- Unicode (\forall)
7#check forall n : Nat, n = n
8
9-- Existential quantifier
10#check ∃ n : Nat, n > 0        -- Unicode (\exists)
11#check Exists (fun n : Nat => n > 0)  -- Prefix form: ∃ is notation for Exists
12
13-- Product types (α and β must be in scope — declare them first)
14variable (α β : Type)
15#check α × β           -- Unicode (\times)
16#check Prod α β        -- Prefix form
17
18-- Lambda
19#check λ x => x + 1    -- Unicode (\l)
20#check fun x => x + 1  -- ASCII
21
22-- Common symbols
23-- ∧ = and  (\and)    ∨ = or   (\or)
24-- ¬ = not  (\neg)    ≠ = ne   (\ne)
25-- ≤ = le   (\le)     ≥ = ge   (\ge)

1-- These are equivalent:
2#check List.length [1, 2, 3]
3#check [1, 2, 3].length        -- Dot notation ✓
4
5#check List.map (fun x => x * 2) [1, 2, 3]
6#check [1, 2, 3].map (fun x => x * 2)  -- Cleaner ✓
7
8-- Chaining operations
9-- |>. continues a chain onto the next line
10#eval [1, 2, 3, 4, 5]
11  |>.filter (· > 2)  -- [3, 4, 5]
12  |>.map (· * 10)    -- [30, 40, 50]
13  |>.reverse         -- [50, 40, 30]
14
15-- String operations
16#eval "Hello World".toUpper.drop 6  -- "WORLD"
17
18-- Works with nested types too
19#eval (some [1, 2, 3]).map List.length  -- some 3

1-- One dot = one parameter
2#eval [1, 2, 3].map (· + 1)          -- [2, 3, 4]
3#eval [1, 2, 3].map (fun x => x + 1) -- same thing
4
5-- Two dots = two parameters, in order of appearance
6#eval [1, 2, 3].foldl (· + ·) 0      -- 6   (fun a b => a + b)
7#eval [2, 1, 3].mergeSort (· ≤ ·)    -- [1, 2, 3]
8
9-- The dots are filled left to right, so order matters
10#eval ([10, 3].foldl (· - ·) 0 : Int)  -- -13, i.e. (0 - 10) - 3

1-- 1. You cannot REUSE an argument. Each · is a fresh parameter,
2--    so (· * ·) is (fun a b => a * b), NOT "square".
3#eval [1, 2, 3].map (fun x => x * x)  -- [1, 4, 9]  ✓ must use fun
4
5-- 2. The lambda extends to the nearest enclosing parentheses.
6--    That is what decides how much of the expression is captured.
7#eval [1, 2, 3].map ((· + 1) * 2)   -- (fun x => x + 1) * 2  — type error
8#eval [1, 2, 3].map (· + 1 |> (· * 2))  -- inner parens make the intent explicit
9#eval [1, 2, 3].map (fun x => (x + 1) * 2)  -- [4, 6, 8]  ✓ clearest

1-- ❌ Wrong: = is for equations/proofs
2-- def x = 5  
3
4-- ✓ Correct: := is for definitions
5def x := 5
6
7-- = is used in propositions
8example : 2 + 2 = 4 := rfl

1-- -> (or →) is for function TYPES
2#check Nat -> Nat     -- A function type
3#check Nat → Nat      -- Same thing
4
5-- => is for lambda BODIES and match arms
6#check fun x => x + 1 -- A lambda expression
7example : Nat -> Nat := fun x => x * 2
8
9-- In match expressions
10def describe (n : Nat) : String :=
11  match n with
12  | 0 => "zero"       -- => in match arms
13  | _ => "positive"

1-- Function application has high precedence
2#check List.map (· + 1) [1, 2, 3]  -- ✓
3-- #check List.map · + 1 [1, 2, 3] -- ❌ Confusing
4
5-- Be explicit when chaining
6#eval (1 + 2) * 3     -- 9
7#eval 1 + 2 * 3       -- 7 (multiplication first)
8
9-- Logical operators
10#check true && false || true   -- (true && false) || true
11#check true && (false || true) -- Explicit is clearer

1#check 2 + 3 * 4      -- parsed as 2 + (3 * 4)
2#check (2 + 3) * 4    -- explicit grouping
3
4#check 1 + 2 + 3      -- left associative: (1 + 2) + 3
5#check 2 ^ 3 ^ 2      -- right associative: 2 ^ (3 ^ 2) = 512
6
7-- Function application is left-associative
8def f (a b c : Nat) : Nat := a + b + c
9#check f 1 2 3        -- parsed as ((f 1) 2) 3
10
11-- Type arrows are right-associative
12#check Nat → Nat → Nat  -- Nat → (Nat → Nat)
13
14-- Which is *why* application is left-associative: f : Nat → (Nat → (Nat → Nat)),
15-- so (f 1) : Nat → Nat → Nat, and ((f 1) 2) : Nat → Nat. The two conventions
16-- fit together so partial application "just works".
17#check f 1            -- Nat → Nat → Nat
18#check f 1 2          -- Nat → Nat

1-- <|  applies the function on the LEFT to everything on the right
2#eval List.length <| List.reverse [1, 2, 3]   -- 3
3#eval List.length (List.reverse [1, 2, 3])    -- same, with parens
4
5-- |>  feeds the value on the LEFT into the function on the right
6#eval [1, 2, 3] |> List.reverse |> List.length  -- 3
7
8-- They compose in a common pattern: pipe the data, apply the last function
9#eval [1, 2, 3] |> List.map (· * 2) |> List.sum   -- 12
10
11-- Both are plain ASCII — no Unicode input needed.
12-- There is also |>. for "pipe into a method": xs |>.reverse |>.length

1-- Pairs
2#check (⟨1, 2⟩ : Nat × Nat)        -- (1, 2)
3#eval  (⟨1, "a"⟩ : Nat × String)   -- (1, "a")
4
5-- It nests, and the nesting can be flattened
6#check (⟨1, 2, 3⟩ : Nat × Nat × Nat)   -- same as ⟨1, ⟨2, 3⟩⟩
7
8-- It only works when the expected type is known.
9-- #check ⟨1, 2⟩          -- error: invalid constructor ⟨...⟩, expected type must be known

1-- s! builds a String, splicing in any value with a ToString instance
2#eval s!"1 + 1 = {1 + 1}"            -- "1 + 1 = 2"
3
4def name := "Ada"
5#eval s!"Hello, {name}! Your name has {name.length} letters."
6
7-- m! is the same idea for messages that may contain expressions (used in
8-- macros and error messages); f! produces formatted output that can wrap.
9-- Escape a literal opening brace with a backslash:
10#eval s!"literal brace: \{ }"      -- "literal brace: { }"

1def greet (name : String) (formal : Bool := false) : String :=
2  if formal then s!"Good day, {name}." else s!"Hey {name}!"
3
4-- Positional
5#eval greet "Alice" true
6
7-- Named (order doesn't matter!)
8#eval greet (formal := true) (name := "Bob")
9
10-- Especially useful with many similar arguments
11def createUser (name : String) (email : String) (age : Nat) := 
12  s!"{name} ({email}), age {age}"
13
14#eval createUser 
15  (name := "Alice") 
16  (email := "[email protected]") 
17  (age := 30)

1-- Forward pipe: passes result to next function
2#eval [1, 2, 3] |> List.reverse |> List.length  -- 3
3
4-- Equivalent to:
5#eval List.length (List.reverse [1, 2, 3])  -- 3
6
7-- Chained example
8def process (xs : List Nat) : Nat :=
9  xs 
10    |> List.filter (· > 0)
11    |> List.map (· * 2)
12    |> List.sum
13
14#eval process [0, 1, 2, 3]  -- 12