[isabelle] `lift_definition (code_dt)` with type classes · Mirror: Isabelle Users Mailing List

I'm seeing an error when attempting to use lift_definition (code_dt)
with type classes. Here is a minimal example:

theory Scratch
    imports Main "HOL-Library.Datatype_Records"
begin

datatype_record 'v foo = blub :: nat

typedef (overloaded) 'a bar = ‹{ m :: 'a foo . True }›
   by (rule_tac x=‹make_foo 0› in exI, simp)
setup_lifting type_definition_bar

lift_definition (code_dt) x :: ‹'v::{default} bar option› is None by
simp
lift_definition (code_dt) y :: ‹'v bar option› is None by simp

(* Lifting failed for the following types:
Raw type:  'v foo option
Abstract type:  'v
x__default_x__x'v_bar_option_x_x_x__default_x__x'v_foo_option

Reason:
   The quotient type "'v
x__default_x__x'v_bar_option_x_x_x__default_x__x'v_foo_option"
     and the quotient type pattern "?'v
x__default_x__x'v_bar_option_x_x_x__default_x__x'v_foo_option"
     don't match. *)

end

Swapping the definitions of x and y 'fixes' things, and so does removing
the type class annotation or using the same annotation in both
definitions.

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] `lift_definition (code_dt)` with type classes

Email Gateway (Feb 18 2024 at 05:13):