Mercurial > hg > Papers > 2021 > soto-prosym
diff Paper/src/agda/syllogism.agda.replaced @ 5:339fb67b4375
INIT rbt.agda
| author | soto <soto@cr.ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Nov 2021 00:51:16 +0900 |
| parents | 9176dff8f38a |
| children |
line wrap: on
line diff
--- a/Paper/src/agda/syllogism.agda.replaced Sat Nov 06 20:06:24 2021 +0900 +++ b/Paper/src/agda/syllogism.agda.replaced Sun Nov 07 00:51:16 2021 +0900 @@ -1,2 +1,2 @@ -syllogism : {A B C : Set} @$\rightarrow$@ ((A @$\rightarrow$@ B) @$\wedge$@ (B @$\rightarrow$@ C)) @$\rightarrow$@ (A @$\rightarrow$@ C) -syllogism x a = _@$\wedge$@_.p2 x (_@$\wedge$@_.p1 x a) +syllogism : {A B C : Set} !$\rightarrow$! ((A !$\rightarrow$! B) !$\wedge$! (B !$\rightarrow$! C)) !$\rightarrow$! (A !$\rightarrow$! C) +syllogism x a = _!$\wedge$!_.p2 x (_!$\wedge$!_.p1 x a)