A common pattern in Arend proofs (apart from ==< equalities >==) is a sequential invocation of functions and metas. A run meta makes these chains comprehensible as can be seen here and here.
However, several ubiquitous callables such as path and function extensionality expect a function as their last argument. This last argument often ends up being a lambda which itself consists of invocations which can be stacked inside run block. This might lead to something known in JS as "callback hell":
run {
lemma1,
path,
\lam i => run {
lemma2,
ext,
\lam x => run {
...
}
}
}
I propose to extend run meta with a <- arrow similar to do-notation in Haskell to escape this callback hell:
run {
lemma1,
i <- path,
lemma2,
x <- ext,
...
}
(One could use a <= arrow instead for consistency with => arrow, but fat left arrow is already used as less-than-or-equals sign)
To be precise, a <- arrow separates a new identifier <id> and an arbitrary expression <e>. After run invocation, all statements after <--statement are put inside a lambda <l> supplied as an argument to <e>; argument of <l> is called <id>.
Note that this also composes nicely with __:
run {
x <- takesLambdaAsFirstArgument __ arg2 arg3
...
}
A common pattern in Arend proofs (apart from
==< equalities >==
) is a sequential invocation of functions and metas. Arun
meta makes these chains comprehensible as can be seen here and here.However, several ubiquitous callables such as
path
and function extensionality expect a function as their last argument. This last argument often ends up being a lambda which itself consists of invocations which can be stacked insiderun
block. This might lead to something known in JS as "callback hell":I propose to extend
run
meta with a<-
arrow similar to do-notation in Haskell to escape this callback hell:(One could use a
<=
arrow instead for consistency with=>
arrow, but fat left arrow is already used as less-than-or-equals sign)To be precise, a
<-
arrow separates a new identifier<id>
and an arbitrary expression<e>
. Afterrun
invocation, all statements after<-
-statement are put inside a lambda<l>
supplied as an argument to<e>
; argument of<l>
is called<id>
.Note that this also composes nicely with
__
: