Re: [isabelle] Type as argument


On Tue, 2011-05-17 at 14:46 +0000, s.wong.731 at 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
> clause? 

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

Kind regards,

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