Eval.Defined

anoma · Jan 15, 2025 · bfa868b · bfa868b
1 parent 35846d2
commit bfa868b
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/Juvix/Core/Main/Semantics/Eval.lean b/Juvix/Core/Main/Semantics/Eval.lean
@@ -55,10 +55,10 @@ inductive Eval (P : Program) : Env → Expr → Value → Prop where
 
 notation "⟨" P "⟩ " env " ⊢ " e " ↦ " v:40 => Eval P env e v
 
-def Terminating (P : Program) (env : Env) (e : Expr) : Prop :=
+def Eval.Defined (P : Program) (env : Env) (e : Expr) : Prop :=
   ∃ v, ⟨P⟩ env ⊢ e ↦ v
 
-notation "⟨" P "⟩ " env " ⊢ " e:40 " ↓" => Terminating P env e
+notation "⟨" P "⟩ " env " ⊢ " e:40 " ↓" => Eval.Defined P env e
 
 -- The evaluation relation is deterministic.
 theorem Eval.deterministic {P env e v₁ v₂} (h₁ : ⟨P⟩ env ⊢ e ↦ v₁) (h₂ : ⟨P⟩ env ⊢ e ↦ v₂) : v₁ = v₂ := by