Mercurial > hg > Members > atton > agda-proofs

changeset 23:723532aa0592

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Test Implicit inference equivalence of function composition
author atton <atton@cr.ie.u-ryukyu.ac.jp>
date Fri, 23 Dec 2016 01:32:17 +0000
parents 84e3fbc662db
children 0fcb7b35ba81
files sandbox/InferenceTypeComposition.agda
diffstat 1 files changed, 11 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/sandbox/InferenceTypeComposition.agda	Fri Dec 23 01:32:17 2016 +0000
@@ -0,0 +1,11 @@
+module InferenceTypeComposition where
+
+open import Relation.Binary.PropositionalEquality
+
+infixl 30 _+++_
+-- _+++_ : {A B C : Set} {equiv : B ≡ B} -> (A -> B) -> (B -> C) -> (A -> C)
+_+++_ : {A B C : Set} -> (A -> B) -> (B -> C) -> (A -> C)
+_+++_ f g = \x -> g (f x)
+
+comp-sample : {A B C D : Set} -> (A -> B) -> (B -> C) -> (C -> D) -> (A -> D)
+comp-sample f g h = f +++ g +++ h