Lang.letExpr

-- let-expressions: local definitions with judgemental transparency.
--
-- The body of `let x = e in b` is typed under x AND its unfolding
-- equation x ≡ e (docs/NovaFoundation.txt, el-let — the strong,
-- definition-carrying form), so facts stated at the abbreviation
-- discharge against facts about its unfolding silently: no manual
-- unfolding, no transport, no plumbing. From the outside a let IS its
-- unfolding (el-let-beta), so lemmas about a let-using definition
-- compute as if the let were never there.
-- checking mode, nested lets, an annotated definiens
-- (`let x : T = e in b` is sugar for `let x = (e : T) in b`)

import Natural (+)

four : ℕ
four = let one : ℕ = S Z in let two = one + one in two + two

-- a let in INFERENCE position (an application head): the body's type
-- is inferred and the definiens substituted back into it
three : ℕ
three = (let f : ℕ → ℕ = λx. S x in f) 2

-- transparency inside the body: the ⋆ pays an equation stated at the
-- ABBREVIATION m while the goal is stated at its unfolding — both
-- gaps close through the let's own hypothesis (m ≡ n + n), not by β
-- (m is a variable, not a redex)
letShared : (n : ℕ) → n + n + Z ≡ n + n using (Natural.plusCongL, Natural.plusZeroId)
letShared = λn. let m = n + n in (⋆ : m + Z ≡ m)

-- the outside view: a let-expression is judgementally its unfolding
fourUnfolds : four ≡ 4 using (Lang.letExpr.four.eq, Natural.+.eq)
fourUnfolds = ⋆

threeUnfolds : three ≡ 3 using (Lang.letExpr.three.eq)
threeUnfolds = ⋆