# HG changeset patch
# User atton <atton@cr.ie.u-ryukyu.ac.jp>
# Date 1482456737 0
# Node ID 723532aa0592a85c2144c9e24e8308c874142217
# Parent  84e3fbc662db7e3a916d15b11037bff6fe01100a
Test Implicit inference equivalence of function composition

diff -r 84e3fbc662db -r 723532aa0592 sandbox/InferenceTypeComposition.agda
--- /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