Re: [isabelle] Want a type of non-negatives for a field, to work like nat/int



On 2/9/2014 4:40 PM, Ondřej Kunčar wrote:
On 02/09/2014 05:28 PM, Gottfried Barrow wrote:
(*NOTE: The "exception TYPE raised" error shown below might be of
interest to someone.)

For example me. Your type definition uses as a raw type a type variable. The new code in lifting that deals with parametricity assumes that the raw type is always a type constructor. I'll take a look at it.

Ondrej,

Thanks. I use `'a::linordered_idom option` as a workaround, as shown below.

NOTE for anyone: I can't get subtype coercion in the Rep direction, as show below. If someone can tell me whether I can or can't do that, I'd appreciate it.


typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None & the x >= 0}"
  by(auto)

(* The Rep declares don't return an error, but have no affect on coercions. *)
(*
declare [[coercion Rep_loidOpt]]
declare [[coercion "Rep_loidOpt::rat loidOpt => rat option"]]

term "(x::rat loidOpt) = Some (y::rat)"
*)

(*Going the Abs direction works, but it's not the subtyping I need.*)

declare [[coercion Abs_loidOpt]]

term "(x::rat loidOpt) = Some (y::rat)"
term "(x::'a::linordered_idom loidOpt) = Some (y::'a::linordered_idom)"

(*I tried messing with coercion_map, but it didn't help.*)

fun MAPloidOpt :: "('a::linordered_idom => 'b::linordered_idom) => 'a loidOpt => 'b loidOpt" where
  "MAPloidOpt f q = Abs_loidOpt(Some(f (the(Rep_loidOpt q))))"

declare [[coercion_map MAPloidOpt]]




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