I'm currently experimenting with pairs/tuples, like the following:
lst :: "((nat*nat)*nat) list"
where ax : "lst = [((1,2),3)]"
lemma "snd (lst ! 0) = (3::nat)"
Does anyone know how I can prove that lemma since sledgehammer can't seem to
find a proof?
Also, if lst was of type "(nat * nat * nat) list", then how do I read the
3rd element from a tuple?
This archive was generated by a fusion of
Pipermail (Mailman edition) and