missing notation

logsem · Jun 12, 2024 · 179a0f0 · 179a0f0
1 parent 39c6ddf
commit 179a0f0
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/examples/delim_lang/logrel.v b/theories/examples/delim_lang/logrel.v
@@ -1227,7 +1227,7 @@ Proof.
 Qed.
 
 Theorem adequacy (e : expr ∅) (k : nat) σ n :
-  (typed_expr □ Tnat e Tnat Tnat) →
+  (empty_env; ℕ ⊢ₑ e : ℕ; ℕ)%type →
   ssteps (gReifiers_sReifier rs) (𝒫 (interp_expr rs e ı_scope)) ([], ())
     (Ret k : IT _ natO) σ n →
   ∃ mm, steps (Cexpr e) (Cret $ LitV k) mm.