[Agda] Termination proof in partiality monad

[Nils Anders Danielsson]

On 2008-11-18 20:43, Dan Doel wrote:
>
> On a related note, I'm seeing things like this in my lower buffer:
> 
>    fix-aux (\_ -> never) fac-aux n | fac-aux (\_ -> never) n)
> 
> (In the 'type' in the error message for instance). What does 'foo | bar' mean? 
> I don't recall ever seeing that before.

With-clauses are usually explained by translating them into simpler
function definitions. However, when proving something about a function
defined using with you do not want to see fresh-name-137 applied to many
arguments. Instead the | notation is used. The meaning of "fun exprs |
expr" is the (substituted) right-hand side of the first clause of fun
where exprs matches the patterns to the left of | and expr matches the
final pattern. (This can be generalised to multiple withs.)

Expressions of the form "fun exprs | expr" can currently only occur in
Agda output. They were planned to be part of the source syntax, but this
has not happened yet.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.