Skip to content

Instantly share code, notes, and snippets.

@jcoglan

jcoglan/case_type.txt

Created May 31, 2017 09:08
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save jcoglan/dfdec933b13490fa80b367ab3e4eec4c to your computer and use it in GitHub Desktop.
Save jcoglan/dfdec933b13490fa80b367ab3e4eec4c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
case_type.txt
# case (inl 0) of inl x ⇒ (iszero x) inr y ⇒ (if y then false else true)
# ----------------------------------------------------------------------
# Bool
------------------------- T-Ctx1 --------------------------- T-Ctx1
(x : Nat) ∈ (∅ , x : Nat) (y : Bool) ∈ (∅ , y : Bool)
----------- T-Zero ------------------------- T-Var --------------------------- T-Var ----------------------------- T-False ---------------------------- T-True
∅ ⊢ 0 : Nat (∅ , x : Nat) ⊢ x : Nat (∅ , y : Bool) ⊢ y : Bool (∅ , y : Bool) ⊢ false : Bool (∅ , y : Bool) ⊢ true : Bool
-------------------------- T-Inl --------------------------------- T-IsZero -------------------------------------------------------------------------------------------------------- T-If
∅ ⊢ (inl 0) : (Nat + Bool) (∅ , x : Nat) ⊢ (iszero x) : Bool (∅ , y : Bool) ⊢ (if y then false else true) : Bool
-------------------------------------------------------------------------------------------------------------------------------------------------------------- T-Case
∅ ⊢ (case (inl 0) of inl x ⇒ (iszero x) inr y ⇒ (if y then false else true)) : Bool
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment