[isabelle] Execute typedef Definition



Dear all,
I am trying to use a "typedef" datatype for code execution.
When I am executing the definition, it fails with an "Abstraction violation".
 
Can I add code-lemmata so that the definition "conv" (see below) is executable?
 
The theory:
typedef evenNat = "{x::nat | x. even x}"
  by auto
setup_lifting type_definition_evenNat
 
definition conv::"nat list evenNat list" where
"conv = map Abs_evenNat o filter even"
 
value "conv [1::nat, 2::nat]" (* Fails with: "Abstraction violation" *)
 
Sincerely,
Sebastian
---------------------------------------------------------------
Sebastian Stüber, M.Sc.RWTH           |    Software Engineering
Lehrstuhl für Software Engineering    |  RWTH Aachen University
Ahornstr. 55, 52074 Aachen, Germany   |  https://www.se-rwth.de
Phone ++49 241 80-21352          
 
 
 

Attachment: Scratch.thy
Description: Scratch.thy



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.