The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 27/04/2016 06:59, Gregory Malecha wrote:
> My understanding is that canonical structures are canonical, i.e. there
> are not multiple solutions to them.

According to this nice half-survey half-tutorial article, you can
actually encode backtracking using canonical structures (Section 8):

https://hal.inria.fr/hal-00816703v2/document

PMP

Attachment: signature.asc
Description: OpenPGP digital signature