Re: [isabelle] Pairs/tuples
On Sun, 2011-04-10 at 19:21 +0100, Steve W wrote:
> I see. But why is 'a of sort "one"?
Because you used the constant 1 in ax. In Isabelle/HOL, the (most
general) type of 1 is 'a::one (rather than, e.g., nat or int).
> Is there a way to declare "lst = (1,2,3)" without fixing the sort?
Well, if 1 was of type 'a (rather than 'a::one), the type of lst in your
axiom would be 'a * nat * nat (rather than 'a::one * nat * nat). For
consts myconst :: 'a
axiomatization lst :: "'a * nat * nat"
axioms ax : "lst = (myconst,2,3)"
lemma "snd (snd lst) = 3"
by (simp add: ax)
However, none of this is very idiomatic. It might be helpful to know
more about what you're actually trying to achieve.
This archive was generated by a fusion of
Pipermail (Mailman edition) and