Re: [isabelle] Type as argument
On Tue, 2011-05-17 at 14:46 +0000, s.wong.731 at gmail.com wrote:
> This is fine. But
> lemma "f b TYPE(nat) = False"
^ There should be a space between f and b.
> by (simp add: f_nat_def)
> doesn't seem to prove it. Can the simplifier not interpret the else
The simplifier doesn't know whether a and b are equal or not. Just
because these two constants have different names, they don't have to be
This archive was generated by a fusion of
Pipermail (Mailman edition) and