Skip to content

Instantly share code, notes, and snippets.

@useronym

useronym/Logic.agda

Created June 26, 2016 12:39
Show Gist options
  • Save useronym/9aa9bd7329b5b98bb6abbf38a32b6ec0 to your computer and use it in GitHub Desktop.
Save useronym/9aa9bd7329b5b98bb6abbf38a32b6ec0 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
Logic.agda
data _and_ (P : Set) (Q : Set) : Set where
_∧_ : P → Q → (P and Q)
∧-elim₁ : {P Q : Set} → (P and Q) → P
∧-elim₁ (p ∧ q) = p
∧-elim₂ : {P Q : Set} → (P and Q) → Q
∧-elim₂ (p ∧ q) = q
∧-comm' : {P Q : Set} → (P and Q) → (Q and P)
∧-comm' (p ∧ q) = q ∧ p
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment