In the file theory/matching-logic.mm, someone can read:
app-is-pattern $a #Pattern ( \app ph0 ph1 ) $.
In the file theory/matching-logic-prelude.mm, someone can read (Part 5):
$c \is-binary-function $.
is-binary-function-is-pattern $a #Pattern ( \is-binary-function ph0 ph1 ph2 ph3 ) $.
${
$d x y z ph0 $.
$d x y z ph1 $.
$d x y z ph2 $.
$d x y z ph3 $.
is-binary-function-is-sugar $a #Notation ( \is-binary-function ph0 ph1 ph2 ph3 )
( \sorted-forall x ph1
( \sorted-forall y ph2
( \sorted-exists z ph3 ( \eq ( \app ph0 x y ) z ) ) ) ) $.
$}
More precisely, I don't understand why it's possible to write: \app ph0 x y.
Is there another definition of \app somewhere that I didn't see?
That's a typo too. It should say ( \app ( \app ph0 x ) y ) instead. This part of the axiom is also not used later so we didn't catch this.
But thanks for pointing this out!!
In the file
theory/matching-logic.mm
, someone can read:In the file
theory/matching-logic-prelude.mm
, someone can read (Part 5):More precisely, I don't understand why it's possible to write:
\app ph0 x y
. Is there another definition of\app
somewhere that I didn't see?