view paper/src/AgdaModusPonens.agda.replaced @ 3:959f4b34d6f4

add final thesis
author soto
date Tue, 09 Feb 2021 18:44:53 +0900
parents
children
line wrap: on
line source

f : {A B C : Set} @$\rightarrow$@ ((A @$\rightarrow$@ B) @$\times$@ (B @$\rightarrow$@ C)) @$\rightarrow$@ (A @$\rightarrow$@ C)
f = \p x @$\rightarrow$@ (snd p) ((fst p) x)