3.1. Type Expressions🔗

Types are base types and function types. The notation #A creates a base type named A, and A ⇒ B is the function type.

A ::= \alpha \mid A \to A

The Lean type below mirrors this grammar. Function arrows associate to the right, so #A ⇒ #B ⇒ #C means #A ⇒ (#B ⇒ #C).

inductive Ty where
  | base (x : String)
  | arr (dom cod : Ty)
deriving DecidableEq, Repr, Lean.ToExpr

syntax:max "#" ident : terminfixr:60 " ⇒ " => Ty.arr

macro_rules
  | `(#$X:ident) => do
      let X' : Lean.TSyntax `term := ⟨Lean.Syntax.mkStrLit X.getId.toString⟩
      `(Ty.base $X')

example : #A ⇒ #B ⇒ #C = #A ⇒ (#B ⇒ #C) := by⊢ Ty.base "A" ⇒ Ty.base "B" ⇒ Ty.base "C" = Ty.base "A" ⇒ Ty.base "B" ⇒ Ty.base "C" rflAll goals completed! 🐙

namespace L2