agda: Move MSFree rule up

hazelgrove · Dec 28, 2023 · 42bc044 · 42bc044
1 parent 25b3710
commit 42bc044
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/core/mexp.agda b/core/mexp.agda
@@ -23,6 +23,11 @@ module core.mexp where
         → (∋x : Γ ∋ x ∶ τ)
         → Γ ⊢⇒ τ
 
+      -- MSFree
+      ⊢⟦_⟧ : ∀ {Γ y}
+        → (∌y : Γ ∌ y)
+        → Γ ⊢⇒ unknown
+
       -- MSLam
       ⊢λ_∶_∙_ : ∀ {Γ τ′}
         → (x : Var)
@@ -78,11 +83,6 @@ module core.mexp where
         → (τ₁⊓τ₂ : τ₁ ⊓ τ₂ ⇒ τ)
         → Γ ⊢⇒ τ
 
-      -- MSFree
-      ⊢⟦_⟧ : ∀ {Γ y}
-        → (∌y : Γ ∌ y)
-        → Γ ⊢⇒ unknown
-
       -- MSInconsistentBranches
       ⊢⦉_∙_∙_⦊[_] : ∀ {Γ τ₁ τ₂}
         → (ě₁ : Γ ⊢⇐ bool)