2.1. Named Syntax🔗

The datatype L1 is the named abstract syntax tree. The notation L1[...] lets examples use lambda-calculus syntax while still elaborating to this datatype.

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

This is the syntax students usually write on paper. The constructors keep the names explicitly, before any quotienting by alpha-equivalence.

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

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

example : L1[λx. x] = L1.lam "x" (L1.var "x") := by⊢ L1.lam "x" (L1.var "x") = L1.lam "x" (L1.var "x") rflAll goals completed! 🐙

example : L1[x y z] = L1[(x y) z] := by⊢ ((L1.var "x").app (L1.var "y")).app (L1.var "z") = ((L1.var "x").app (L1.var "y")).app (L1.var "z") rflAll goals completed! 🐙