changeset 77:a2e6f61d5f2b default tip

Add modus-ponens
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Thu, 09 Feb 2017 06:32:03 +0000
parents 29a3a4b79d4d
children
files sandbox/modus-ponens.agda
diffstat 1 files changed, 13 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sandbox/modus-ponens.agda	Thu Feb 09 06:32:03 2017 +0000
@@ -0,0 +1,13 @@
+module modus-ponens where
+
+data _×_ (A B : Set) : Set where
+  <_,_> : A -> B -> A × B
+
+fst : {A B : Set} -> A × B -> A
+fst < a , _ > = a
+
+snd : {A B : Set} -> A × B -> B
+snd < _ , b > = b
+
+f : {A B C : Set} -> (A -> B) × (B -> C) -> (A -> C)
+f = (\p x -> snd p ((fst p) x))