Re: [isabelle] Type as argument



Steve,

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
> 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
distinct.

Kind regards,
Tjark







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