Re: [isabelle] Specification depends on extra type variables
Thank you for your answer. Almost for sure I would have an inconsistency
to what you showed if I would use the axiomatic approach. I have used
to introduce the extra types. Moreover, my definition depends also on a
(pair) and I fixed that in the locale too.
This solution is satisfactory, but reading your example, I realized that
what I would
need is an existential quantification on the extra type:
axioms f_def2: "f (a::'a) = (EX 'b::type . (EX (g::'b => 'a). inj g))"
Like this there is no danger of inconsistencies. Is there something in
would allow something similar to this?
If you really want to avoid explicitly passing around an extra dummy
parameter, here's what I would recommend: Declare a locale that fixes
the dummy type parameter of type "'b itself", and define your
constants (which may refer to the locally-fixed type 'b) inside the
This archive was generated by a fusion of
Pipermail (Mailman edition) and