Skip to content

Instantly share code, notes, and snippets.

@jcoglan

jcoglan/let_types.txt

Created May 25, 2017 13:42
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/7ee803ebd9fe0f6990e1641ca4b1a211 to your computer and use it in GitHub Desktop.
Save jcoglan/7ee803ebd9fe0f6990e1641ca4b1a211 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
let_types.txt
--------------------------- T-Ctx1
(x : Bool) ∈ (∅ , x : Bool)
---------------------------------------- T-Ctx2 ---------------------------------------- T-Ctx1
(x : Bool) ∈ ((∅ , x : Bool) , y : Bool) (y : Bool) ∈ ((∅ , x : Bool) , y : Bool)
---------------------------------------- T-Var ---------------------------------------- T-Var
((∅ , x : Bool) , y : Bool) ⊢ x : Bool ((∅ , x : Bool) , y : Bool) ⊢ y : Bool
----------------------------------------------------------------------------------------- T-Pair
((∅ , x : Bool) , y : Bool) ⊢ (x , y) : (Bool × Bool)
---------------------------------------------------------------- T-Abs
(∅ , x : Bool) ⊢ (λ y : Bool . (x , y)) : (Bool → (Bool × Bool))
--------------------------------------------------------------------------- T-Abs --------------- T-True
∅ ⊢ (λ x : Bool . (λ y : Bool . (x , y))) : (Bool → (Bool → (Bool × Bool))) ∅ ⊢ true : Bool
-------------------------------------------------------------------------------------------------- T-App ---------------- T-False
∅ ⊢ ((λ x : Bool . (λ y : Bool . (x , y))) true) : (Bool → (Bool × Bool)) ∅ ⊢ false : Bool
----------------------------------------------------------------------------------------------------------------- T-App
∅ ⊢ (((λ x : Bool . (λ y : Bool . (x , y))) true) false) : (Bool × Bool)
------------------------------------------------------------------------ T-Proj2
∅ ⊢ ((((λ x : Bool . (λ y : Bool . (x , y))) true) false) . 2) : Bool
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment