[Agda] Q: Equational Reasoning

[Nils Anders Danielsson]

On 2009-05-27 15:14, Conor McBride wrote:
> 
> The point is that it uses a recursive problem-solving
> strategy which is beyond the power of Agda's termination
> checker to recognize, but not beyond the power of type
> theory to explain. I ended up writing a hand-elaborated
> Epigram program in Agda's expression language.

Variants of some of Conor's memo structures are available in the
standard library (under Induction). For examples of how these structures
can be used, see, for instance,
http://www.cs.nott.ac.uk/~nad/listings/lib/Induction.Lexicographic.html
and
http://www.cs.nott.ac.uk/~nad/listings/lib/Data.Nat.GCD.html.

-- 
/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.