Checking first-order languages like:
check Γ BOOL (forAll body) =
check (BOOL ∷ Γ) BOOL body ∨
check (INT ∷ Γ) BOOL body
Checking first-order languages like:
check Γ BOOL (forAll body) =
check (BOOL ∷ Γ) BOOL body ∨
check (INT ∷ Γ) BOOL body