1.1. Syntax🔗

The terms of L0 are variables, free variables, lambda abstractions, and applications.

e ::= n \mid x \mid \lambda.\ e \mid e\ e

The Lean datatype below has one constructor for each form in this grammar.

inductive L0 where
  | var (x : Nat)
  | free (x : String)
  | lam (body : L0)
  | app (fn arg : L0)
deriving DecidableEq, Repr, Lean.ToExpr

syntax_rules l0Term quoted_by "L0[" l0Term "]" where
  | "{" t:term "}"          => t
  | "(" t:l0Term ")"        => parse t
  | n:num                   => L0.var n
  | x:ident                 => L0.free x
  | "λ" body:l0Term         => L0.lam (parse body)
  | f:l0Term:70 a:l0Term:71 => L0.app (parse f) (parse a)

example : L0[x] = .free "x" := by⊢ L0.free "x" = L0.free "x" rflAll goals completed! 🐙

example : L0[λ λ 1] = .lam (.lam (.var 1)) := by⊢ (L0.var 1).lam.lam = (L0.var 1).lam.lam rflAll goals completed! 🐙

example : L0[0 1 2] = .app (.app (.var 0) (.var 1)) (.var 2) := by⊢ ((L0.var 0).app (L0.var 1)).app (L0.var 2) = ((L0.var 0).app (L0.var 1)).app (L0.var 2) rflAll goals completed! 🐙

namespace L0