Skip to content

Instantly share code, notes, and snippets.

@louisswarren
Last active April 10, 2018 09:30
Show Gist options
  • Select an option

  • Save louisswarren/e875a473492890f775b752889303e0c0 to your computer and use it in GitHub Desktop.

Select an option

Save louisswarren/e875a473492890f775b752889303e0c0 to your computer and use it in GitHub Desktop.
Syntax is fun (don't actually do this)
data _⊢_ : List Formula → Formula → Set where
assume : (α : Formula) → [ α ] ⊢ α
arrowintro : ∀{Γ β} → (α : Formula) → Γ ⊢ β
--------------- ⇒+ α
→ Γ ∖ α ⊢ α ⇒ β
arrowelim : ∀{Γ₁ Γ₂ α β} → Γ₁ ⊢ α ⇒ β → Γ₂ ⊢ α
--------------------------- ⇒-
→ (Γ₁ ++ Γ₂) ⊢ β
@louisswarren
Copy link
Author

But actually do do this.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment