let-expressions in the element language

docs/NovaElaboration.txt

@@ -145,6 +145,10 @@ T{0} ::= t{≥2} ≡ t{≥2} ∈ T{≥1}
 t{5} ::= x | () | Z | ⋆ | ∥T{≥0}∥ | 𝟘 | 𝟙 | ℕ | (t{≥0}) | (t{≥0} : T{≥0})
 t{3} ::= t{≥3} t{≥4} | t{≥3} .π₁ | t{≥3} .π₂                 (left-assoc)
 t{2} ::= λx. t{≥1½}
+       | let x ≔ t{≥0} in t{≥1½}                              # let-expression
+       | let x : T{≥0} ≔ t{≥0} in t{≥1½}                      #   (annotated
+                                                              #   definiens) —
+                                                              #   see e-let
        | 𝟘-elim t{≥4}
        | S t{≥4}
        | ℕ-elim (n. T{≥0}) t{≥4} (n ih. t{≥4}) t{≥4}          # motive, z, s, scrutinee
@@ -306,7 +310,8 @@ instead an error asking the user for an ascription or annotation.
 //////// whnf ////////
 
 whnf(–) is weak-head normalization by Foundation's ≜ rules:
-el-pi-beta, el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z,
+el-pi-beta, el-let-beta (a let is always a redex — no whnf ever
+returns one), el-sigma-beta₁, el-sigma-beta₂, el-nat-beta-z,
 el-nat-beta-s, el-sum-beta₁, el-sum-beta₂, el-quot-beta,
 el-nu-beta (out at a corec head — map_𝔽 and hᵉˡ expanding by
 Foundation's ≜-clauses), el-qiit-beta (the eliminator at a
@@ -428,6 +433,21 @@ componentwise at F ⨯ G and F ⊎ G                  (e-poly-prod, e-poly-sum)
 ---------------------- (e-ann)
 Γ ⊢ (t : T) ⇒ A ⇝ t̂
 
+Γ ⊢ e ⇒ A ⇝ ê
+Γ ▷ x:A ▷ h:Prf (☐₀ ≡ ê[↑] ∈ A[↑]) ⊢ b ⇒ B ⇝ b̂
+-------------------------------------------------- (e-let)    # (let a b)
+Γ ⊢ let x ≔ e in b ⇒ B[id, ê, ⋆] ⇝ let ê b̂
+# The DEFINIENS is inferred — a checking-only definiens (λ, pair, ...)
+# takes the annotated form, which is parse-level sugar for ascription:
+#     let x : T ≔ e in b   ≜   let x ≔ (e : T) in b
+# The BODY is elaborated under x AND the unfolding hypothesis h. h's
+# type is a Prf of an equality prop, so E's HYPOTHESIS source reflects
+# ☐₁ ≐ ê[↑ ∘ ↑] into discharge automatically: the definition is
+# TRANSPARENT inside the body with no new mechanism — Foundation's
+# el-let, the definition-carrying-context reading. h never appears in
+# b (nothing binds it on the surface); it exists for discharge and for
+# the kernel's context, and the report printer renders it silently.
+
 Γ ▷ n:ℕ ⊢ T ⇝ A type
 Γ ⊢ z ⇐ A[id, Z] ⇝ ẑ
 Γ ▷ n:ℕ ▷ ih:A ⊢ s ⇐ A[↑ ∘ ↑, S ☐₁] ⇝ ŝ
@@ -692,6 +712,17 @@ whnf(C) = Prf ∥A∥        Γ ⊢ e ⇐ A ⇝ ê
 # Any expected C; 𝟘-elim is the one form that checks against
 # everything. In inference position it is a structural error (ascribe).
 
+Γ ⊢ e ⇒ A ⇝ ê
+Γ ▷ x:A ▷ h:Prf (☐₀ ≡ ê[↑] ∈ A[↑]) ⊢ b ⇐ C[↑ ∘ ↑] ⇝ b̂
+--------------------------------------------------------- (e-let-check)
+Γ ⊢ let x ≔ e in b ⇐ C ⇝ let ê b̂
+# let PROPAGATES the ambient mode to its body — this direct checking
+# rule (rather than e-let + e-switch) is what lets a checking-only
+# body form (a λ, a pair, a ⋆) sit under a let without ascription.
+# C lives over Γ, so checking b at C[↑ ∘ ↑] is fully general, not an
+# approximation (docs/NovaKernel.txt §8, el-let). The definiens and
+# the hypothesis are exactly as at e-let.
+
 Γ ⊢ t ⇒ B ⇝ t̂        Γ ⊢ B ≐ C type ↓
 --------------------------------------- (e-switch)
 Γ ⊢ t ⇐ C ⇝ t̂
@@ -705,7 +736,9 @@ whnf(C) = Prf ∥A∥        Γ ⊢ e ⇐ A ⇝ ê
 # squash-elim, 𝟘-elim (their types are not determined by their syntax
 # — an injection alone does not determine the OTHER summand);
 # encountering one in inference position is a structural error whose
-# fix is an ascription. Everything else — including ∥-∥ — infers and
+# fix is an ascription. let is BOTH-MODE: its body elaborates in the
+# ambient mode (e-let / e-let-check), its definiens always in
+# inference mode. Everything else — including ∥-∥ — infers and
 # reaches checking mode through e-switch.
 
 //////////// Conversion and discharge (the ↓ judgements) /////////////

docs/NovaFoundation.txt

@@ -1,6 +1,6 @@
 ////////// Preface //////////
 
-#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map
+#! highlight keywords: ⊦ : ; , · [ ] ‖ .π₁ .π₂ ∈ ∋ ≐ ≜ ≔ ⇒ ⇐ = ⬡ ⬦ ▷ ◁ ⇛ ⇑ 𝕚𝕕 El U ☐ ε ↑ ∘ ⁺ id λ let → ⨯ ⊎ ≡ ∥ / Ω 𝕌 ℕ 𝟘 𝟙 Z S ⋆ Prf class inj₁ inj₂ ⌊ ⌋ ⟦ ⟧ ⋈ ⋉ ᴰ 𝟘-elim ℕ-elim quot-elim squash-elim ⊎-elim -elim qctx qty qsig ctx type tel mot dalg eprob sect norm small sig nf qpath ν 𝕏 K out corec poly map
 #! highlight tos: 𝔄 𝔅 𝕥 𝕦 𝕧 𝕤 𝕔 𝕜 𝕘 𝕒 𝕓 𝕞 Φ 𝒮 ς 𝔎 𝔽 𝔾
 #! highlight nova: Γ Δ Ξ Σ σ τ δ θ latin
 #! highlight meta: 𝑤 ρ υ π 𝒞 ℰ
@@ -146,6 +146,9 @@ t ::= x [e˲]         # element in the signature context
     | ☐ᵢ             # i-th element in the typing context
     | λ t            # dependent product type introduction
     | t t            # dependent product type elimination
+    | let t t        # let-expression (definiens, body — the body
+                     #   binds the definiens AND its unfolding
+                     #   equation; see the let block)
     | t , t          # dependent sum type introduction
     | t .π₁          # dependent sum type elimination (1)
     | t .π₂          # dependent sum type elimination (2)
@@ -1064,6 +1067,36 @@ e˲ : Γ₁ ⇒ Γ norm
 --------------------------------- (el-pi-eta)
 Γ ⊦ λ (f[↑] ☐₀) ≐ f : A → B
 
+# let — the local DEFINITION: the body is typed under TWO binders,
+# the definiens' value and its UNFOLDING EQUATION, so inside b the
+# definiendum unfolds judgementally — el-reflect on ☐₀ gives
+# ☐₁ ≐ a[↑ ∘ ↑] : A[↑ ∘ ↑]. This is a definition-carrying context
+# discipline (Γ ▷ (x ≔ a : A)) with NO new context former:
+# extensionally a definition IS a variable plus a Prf of its
+# unfolding — the same degeneration that collapses the QIIT
+# coherence tower. el-let-beta unfolds the whole expression to the
+# instantiated body, the ⋆ typed by el-eq-i at the reflexive
+# instance a ≡ a, so a let and its unfolding are interchangeable
+# everywhere. NOT a type former — nothing is introduced or
+# eliminated, hence no eta and no injectivity — and DEFINABLE:
+# let a b ≐ ((λ (λ b)) a) ⋆ (two el-pi-beta steps compute the
+# encoding to b[id, a, ⋆]; ty-pi forms its Π-types from the
+# premises' presuppositions). Retained like ℕ and (/) for
+# convenience, not necessity — here the convenience is SYNTACTIC
+# IDENTITY: a local definition should read (and print) as one, not
+# as its λ-plumbing. A body that ignores the equation just weakens
+# past ☐₀ — the "weak" (opaque-binder) let is the special case.
+
+Γ ⊦ a : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+------------------------------------------ (el-let)
+Γ ⊦ let a b : B[id, a, ⋆]
+
+Γ ⊦ a : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+---------------------------------------------- (el-let-beta)
+Γ ⊦ let a b ≜ b[id, a, ⋆] : B[id, a, ⋆]
+
 # Σ.
 
 Γ ▷ A ⊦ B type
@@ -2139,6 +2172,15 @@ e˲ : Δ ⇒ Γ norm
 ------------------------------------------ (el-sub-app)
 Γ₀ ⊦ (f e)[σ] ≜ f[σ] e[σ] : B[σ, e[σ]]
 
+Γ₁ ⊦ a : A
+Γ₁ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b : B
+σ : Γ₀ ⇒ Γ₁
+------------------------------------------------------- (el-sub-let)
+Γ₀ ⊦ (let a b)[σ] ≜ let a[σ] b[σ⁺⁺] : B[σ, a[σ], ⋆]
+# (coherent: ☐₀[σ⁺] ≜ ☐₀ and a[↑][σ⁺] ≐ a[σ][↑], so the Prf entry
+# lands as the unfolding equation OF a[σ] — the RHS is the let at
+# a[σ] — and ⋆[σ] ≜ ⋆ keeps the conclusion type in shape)
+
 Γ₁ ▷ A ⊦ B type
 Γ₁ ⊦ a : A
 Γ₁ ⊦ b : B[id, a]
@@ -2291,6 +2333,14 @@ e˲ : Γ₁ ⇒ Γ norm
 ------------------------------------ (el-app-cong)
 Γ ⊦ f₀ a₀ ≐ f₁ a₁ : B[id, a₁]
 
+Γ ⊦ a₀ ≐ a₁ : A
+Γ ▷ A ▷ Prf (☐₀ ≡ a₁[↑] ∈ A[↑]) ⊦ b₀ ≐ b₁ : B
+--------------------------------------------------- (el-let-cong)
+Γ ⊦ let a₀ b₀ ≐ let a₁ b₁ : B[id, a₁, ⋆]
+# (the a₀- and a₁-instance contexts are equal — ctx-ext-cong with
+# code-eq-cong — so the premise is stated at the a₁ instance, as at
+# the other congruences)
+
 Γ ▷ A ⊦ B type
 Γ ⊦ a₀ ≐ a₁ : A
 Γ ⊦ b₀ ≐ b₁ : B[id, a₁]

docs/NovaKernel.txt

@@ -49,6 +49,9 @@ are not listed; the contraction clauses, each of which burns one unit
 of fuel, are exactly:
 
   (λ f) e            ≜  f[id, e]                    # el-pi-beta
+  let a b            ≜  b[id, a, ⋆]                 # el-let-beta (a let is
+                                                    # ALWAYS a redex: normal
+                                                    # forms contain no let)
   (a , b) .π₁        ≜  a                           # el-sigma-beta₁
   (a , b) .π₂        ≜  b                           # el-sigma-beta₂
   ℕ-elim z s Z       ≜  z                           # el-nat-beta-z
@@ -201,6 +204,7 @@ Child indexing, shared by paths, the typed descent (§6) and skeletons
   elements:  𝟘-elim t → 0            S t → 0
              ℕ-elim z s t → 0, 1(2), 2
              λ f → 0(1)              f e → 0, 1
+             let a b → 0, 1(2)       # body under value + unfolding-Prf binders
              (a , b) → 0, 1          t.π₁ / t.π₂ → 0
              inj₁ t / inj₂ t → 0     ⊎-elim l r t → 0(1), 1(1), 2
              a →ᶜ b → 0, 1(1)        a ⨯ᶜ b → 0, 1(1)
@@ -327,6 +331,12 @@ introduction forms structurally and falls back to infer-and-compare:
 Signature substitutions e˲ ⇐ᵖ Δ are checked entrywise, entry i's
 telescope type instantiated by the preceding entries (sub-norm-ext).
 
+let-expressions are NOT in the proof fragment (neither ⇒ᵖ nor ⇐ᵖ):
+a license containing one is rejected. Nothing is lost — a let is
+always a redex (§1), so the elaborator emits licenses let-free;
+a lemma whose body wants one is referenced through Σ, where the
+item level checks lets directly (§8).
+
 ////////// 4. What a step licenses //////////
 
 A step (onLhs, path, lic, sels, flip) licenses one equation, derived —
@@ -433,6 +443,9 @@ type E; — means undetermined):
                   child 1 : E[↑][↑]      # ditto
                   child 2 : ℕ
   λ f             child 0 : B            when nf(E) ⇓ A → B
+  let a b         (never reached: replay normalizes both sides before
+                   any step (§7) and a let is always a redex (§1), so
+                   no rewrite path meets one)
   f e             child 0 : —
                   child 1 : A            when f is an inferable spine
                                          # ⇒ᴺ, below
@@ -600,6 +613,17 @@ Checking  Σ; Γ ⊦ t ⇐ T ⟨sk⟩ :
      -----------------------------------------          # el-pi-i
      Σ; Γ ⊦ λ f ⇐ T ⟨sk⟩
 
+     Σ; Γ ⊦ a ⇒ A ⟨sk.0⟩
+     Σ; Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b ⇐ T[↑ ∘ ↑] ⟨sk.1⟩
+     --------------------------------------------------------
+     Σ; Γ ⊦ let a b ⇐ T ⟨sk⟩                            # el-let
+     # T lives over Γ, so checking b at T[↑ ∘ ↑] is fully general,
+     # not an approximation: under the unfolding hypothesis
+     # (id, a, ⋆) ∘ (↑ ∘ ↑) ≐ id (el-reflect on ☐₀ plus el-prf-prop),
+     # so any valid body type is ≐ T[↑ ∘ ↑]. The definiens is
+     # INFERRED — an intro-form definiens carries intro-ty on sk.0,
+     # the ascription route.
+
      nf(T) ⇓ A ⨯ B    Σ; Γ ⊦ u ⇐ A ⟨sk.0⟩   Σ; Γ ⊦ v ⇐ B[id,u] ⟨sk.1⟩
      ---------------------------------------------------------------
      Σ; Γ ⊦ (u , v) ⇐ T ⟨sk⟩                            # el-sigma-i
@@ -684,6 +708,13 @@ Inference  Σ; Γ ⊦ t ⇒ T ⟨sk⟩ :
 
      (projections analogously: el-sigma-e₁/₂)
 
+  let infers when its body does (definiens inferred, as in checking):
+
+     Σ; Γ ⊦ a ⇒ A ⟨sk.0⟩
+     Σ; Γ ▷ A ▷ Prf (☐₀ ≡ a[↑] ∈ A[↑]) ⊦ b ⇒ B ⟨sk.1⟩
+     ------------------------------------------------------------
+     Σ; Γ ⊦ let a b ⇒ B[id, a, ⋆]                       # el-let
+
   ℕ-elim demands its motive — the REAL rule, no approximation here:
 
      sk carries motive M ⟨skM⟩       Σ; Γ ▷ ℕ ⊦ M type ⟨skM⟩

src/idris/Nova/Compute.idr

@@ -129,6 +129,8 @@ mutual
     case whnfElem sig f of
       PiIntro g => whnfElem sig (substElem g (Ext Id e))
       _ => assert_total $ idris_crash "whnfElem: application head is not a function (impossible for a closed, well-typed term)"
+  -- el-let-beta: a let is ALWAYS a redex
+  whnfElem sig (Let a b) = whnfElem sig (substElem b (Ext (Ext Id a) Star))
   whnfElem sig (SigmaIntro a b)   = SigmaIntro a b
   whnfElem sig (SigmaElim1 t) =
     case whnfElem sig t of
@@ -255,6 +257,7 @@ mutual
     go (Elem.EqTy l r t)  = Elem.EqTy (nfElem sig l) (nfElem sig r) (nfTy sig t)
     go (QuotTy a r)       = QuotTy (nfElem sig a) r   -- r: under a binder, left alone
     go (SigVar x es)      = SigVar x es   -- unreachable: whnf always unfolds x[e˲]
+    go (Let a b)          = Let a b   -- unreachable: whnf always contracts a let
     go (Class a)          = Class (nfElem sig a)
     go (QuotElim f q)     = QuotElim f (nfElem sig q)   -- f: under a binder, left alone
     go (Squash t)         =

src/idris/Nova/Elaboration.idr

@@ -251,6 +251,7 @@ mapRefsE f (NatIntro1 t) = NatIntro1 (mapRefsE f t)
 mapRefsE f (NatElim z s t) = NatElim (mapRefsE f z) (mapRefsE f s) (mapRefsE f t)
 mapRefsE f (PiIntro g) = PiIntro (mapRefsE f g)
 mapRefsE f (PiApp g e) = PiApp (mapRefsE f g) (mapRefsE f e)
+mapRefsE f (Let a b) = Let (mapRefsE f a) (mapRefsE f b)
 mapRefsE f (SigmaIntro a b) = SigmaIntro (mapRefsE f a) (mapRefsE f b)
 mapRefsE f (SigmaElim1 t) = SigmaElim1 (mapRefsE f t)
 mapRefsE f (SigmaElim2 t) = SigmaElim2 (mapRefsE f t)
@@ -333,6 +334,7 @@ collectRefsE e = go e
   go (NatElim z s t) = go z ++ go s ++ go t
   go (PiIntro f) = go f
   go (PiApp f x) = go f ++ go x
+  go (Let a b) = go a ++ go b
   go (SigmaIntro a b) = go a ++ go b
   go (SigmaElim1 t) = go t
   go (SigmaElim2 t) = go t
@@ -737,6 +739,7 @@ elemSize (NatIntro1 t) = S (elemSize t)
 elemSize (NatElim z s t) = S (elemSize z + elemSize s + elemSize t)
 elemSize (PiIntro f) = S (elemSize f)
 elemSize (PiApp f e) = S (elemSize f + elemSize e)
+elemSize (Let a b) = S (elemSize a + elemSize b)
 elemSize (SigmaIntro u v) = S (elemSize u + elemSize v)
 elemSize (SigmaElim1 t) = S (elemSize t)
 elemSize (SigmaElim2 t) = S (elemSize t)
@@ -1818,6 +1821,8 @@ mutual
     case zonkElem st f of
       PiIntro g => zonkElem st (substElem g (Ext Id e))
       f2 => PiApp f2 (zonkElem st e)
+  -- el-let-beta: a let is always a redex
+  zonkElem st (Let a b) = zonkElem st (substElem b (Ext (Ext Id a) Star))
   zonkElem st (SigmaIntro a b) = SigmaIntro (zonkElem st a) (zonkElem st b)
   zonkElem st (SigmaElim1 t) =
     case zonkElem st t of
@@ -3008,6 +3013,17 @@ mutual
     (ty', tySk) <- elabTy ctx env site ty
     (t', tSk) <- checkElem ctx env site t ty'
     pure (t', ty', addPayload (PIntroTy ty' tySk) tSk)
+  inferElem ctx env site (SLet (x, xr) e b) = do
+    -- e-let: the definiens is INFERRED (an annotated surface let
+    -- arrives as an ascribed definiens); the body is elaborated under
+    -- the value AND its unfolding hypothesis — a Prf of an equality
+    -- prop, so E's HYPOTHESIS source reflects x ≐ e into discharge
+    -- automatically: the definition is transparent inside the body
+    (e', eTy, eSk) <- inferElem ctx env site e
+    recordBinder xr ctx env x eTy
+    let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem e' Wk) (substTy eTy Wk))
+    (b', bTy, bSk) <- inferElem (ctx :< eTy :< hyp) (env :< x :< wildcard) site b
+    pure (Let e' b', substTy bTy (Ext (Ext Id e') Star), Nd [] [eSk, bSk])
   inferElem ctx env site (SNatElim (n, nr) mot z (n2, n2r) (ih, ihr) s t) = do
     recordBinder nr ctx env n Ty.NatTy
     (motTy, motSk) <- elabTy (ctx :< Ty.NatTy) (env :< n) site mot
@@ -3355,6 +3371,18 @@ mutual
         modifySt $ { sig $= (:< SigDecl ctx q ty)
                    , holeMeta $= (:< MkHoleMeta q env site solvable mrng) }
         pure (SigVar q (idSpine (length ctx)), baseSk)
+  checkElem ctx env site (SLet (x, xr) e b) ty = do
+    -- e-let-check: let PROPAGATES the ambient mode to its body (a
+    -- checking-only body form works under a let without ascription).
+    -- The expected type lives over Γ, so the body checks at its double
+    -- weakening — fully general, not an approximation (docs/
+    -- NovaKernel.txt §8, el-let)
+    (e', eTy, eSk) <- inferElem ctx env site e
+    recordBinder xr ctx env x eTy
+    let hyp = Prf (Elem.EqTy (CtxVar 0) (substElem e' Wk) (substTy eTy Wk))
+    (b', bSk) <- checkElem (ctx :< eTy :< hyp) (env :< x :< wildcard) site b
+                   (substTy (substTy ty Wk) Wk)
+    pure (Let e' b', Nd [] [eSk, bSk])
   checkElem ctx env site t ty = do
     (t', inferred, tSk) <- inferElem ctx env site t
     c <- convTy ctx env "\{site}: inferred vs expected type" Nothing inferred ty

src/idris/Nova/Elaboration/Named.idr

@@ -241,6 +241,7 @@ mutual
   usesIndexElem k (NatElim z s t) = usesIndexElem k z || usesIndexElem (S (S k)) s || usesIndexElem k t
   usesIndexElem k (PiIntro e) = usesIndexElem (S k) e
   usesIndexElem k (PiApp f e) = usesIndexElem k f || usesIndexElem k e
+  usesIndexElem k (Let a b) = usesIndexElem k a || usesIndexElem (S (S k)) b
   usesIndexElem k (SigmaIntro e e') = usesIndexElem k e || usesIndexElem k e'
   usesIndexElem k (SigmaElim1 e) = usesIndexElem k e
   usesIndexElem k (SigmaElim2 e) = usesIndexElem k e
@@ -363,6 +364,15 @@ mutual
   prettyElemPrefixN tbl env (PiIntro e) =
     let x = freshGeneric env
     in "λ" ++ x ++ ". " ++ prettyElemOpN tbl (env :< x) 0 e
+  prettyElemPrefixN tbl env (Let a b) =
+    -- surface-faithful: the unfolding-equation binder has no surface
+    -- spelling and elaborator-produced bodies never reference it; it
+    -- still enters the env (under a fresh Prf-flavored name) so a
+    -- reference in hand-built core would at least print visibly
+    let x = freshGeneric env
+        h = freshFromList candidatesPrf (env :< x)
+    in "let " ++ x ++ " ≔ " ++ prettyElemN tbl env a ++ " in "
+         ++ prettyElemOpN tbl (env :< x :< h) 0 b
   prettyElemPrefixN tbl env (ZeroElim e) = "𝟘-elim " ++ prettyElemAtomN tbl env e
   prettyElemPrefixN tbl env (NatIntro1 e) = "S " ++ prettyElemAtomN tbl env e
   prettyElemPrefixN tbl env (NatElim z s t) =