view paper/src/AgdaModusPonens.agda.replaced @ 2:c7acb9211784

add code, figure. and paper fix content
author ryokka
date Mon, 27 Jan 2020 20:41:36 +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)