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



On 2/10/2014 8:15 AM, Dmitriy Traytel wrote:
This is out of scope for (1). The incompleteness of (2) is visible on your example, which only will not insert coercions in the first argument of equality (and of other polymorphic functions). It would have worked if you had reversed the equation:

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

Thanks. It's fortunate I didn't switch the order, or in the future it could have been, "I thought I remember that this worked."

If Ondrej accommodates, the problem I show next won't be an issue, but below, I show how I can coerce to `rat`, but not to `'a::linordered_idom`.

And thanks for the explanation. Guessing here, from what you said and what Ondrej said, the error below is because the coercion needs a type constructor, and `'a::linordered_idom` is only a type variable.

Are there such things as 0-ary type constructor variables, that I can put in place of `'a`? With `show_sorts`, I never see the type/sort of `nat` or `int`.

(*source with error*)
typedef ('a::linordered_idom) loidOpt = "{x::'a option. x ~= None & the x >= 0}"
  by(auto)
declare [[coercion Rep_loidOpt]]

definition the_Rep_loidOpt :: "'a::linordered_idom loidOpt => 'a" where
  "the_Rep_loidOpt x = the(Rep_loidOpt x)"

declare [[coercion "the_Rep_loidOpt::rat loidOpt => rat"]]

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

declare [[coercion the_Rep_loidOpt]]
(*
Bad type for a coercion:
the_Rep_loidOpt :: ?'a::linordered_idom loidOpt => ?'a::linordered_idom
*)

Thanks again,
GB




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