[Agda] Automatic generation of trivial proofs

[Christoph Herrmann]

Hi all,

as you probably know, Agda is happy with a refl if it can figure out an equality just by
evaluation. I have come across the problem to prove equations on  combinations
of enumeration types. An example Agda script is attached in which I prove a property
of a boolean function, using the *All* data type described in Ulf Norell's AFP'08 tutorial.

Note that the "rubbish" at the right-hand side of "AutoProof" was generated
automatically by typing Ctrl-C Ctrl-A into a goal. Agda would of course
not provide a proof if the predicate was incorrect.

My question: is it possible to tell Agda it does not need to pollute the program text with that
kind of rubbish? For some reason Agda turns just an underscore into yellow which is not
sufficient for verification.

Cheers

-------------- next part --------------
A non-text attachment was scrubbed...
Name: AutoProof.agda
Type: application/octet-stream
Size: 861 bytes
Desc: not available
Url : http://lists.chalmers.se/pipermail/agda/attachments/20110305/dce883c2/AutoProof.obj
-------------- next part --------------

--
 Dr. Christoph Herrmann
 University of St Andrews, Scotland/UK
 phone: office: +44 1334 461629, home: +44 1334 478648 
 email: ch at cs.st-andrews.ac.uk,  c.herrmann at virgin.net
 URL:   http://www.cs.st-andrews.ac.uk/~ch
 
 The University of St Andrews is a charity registered in Scotland: No SC013532