Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Problem with inductive predicate code generati...

Email Gateway (Aug 22 2022 at 20:53):

From: Mark Wassell <mpwassell@gmail.com>
Hello,

I am having a couple of problems generating code from inductive predicates
that involve a type synonym. Attached is a theory file with examples but
here is a summary:

Problem 1. The type synonym is a pair and attempting to use fst in the
definition of the predicate results in

exception MATCH raised (line 369 of "pattern.ML")

Defining a monomorphic version of fst gets around this problem.

Problem 2. If I have a slightly different form for the predicate then I get
a 'proof failed' error. The fact that it is attempting to prove can easily
be proved with simp.

Cheers

Mark
CodeGenQuery.thy

Last updated: Apr 26 2024 at 12:28 UTC