Re: [isabelle] What is sumC?



> That doesn't work. When I type in:
> lemma "fact 3 = 6" unfolding eval_nat_numeral BitM.simps by simp
> I get the message:
> Failed to apply initial proof method: goal (1 subgoal): 1. fact 3 = 6

Can you give the definition of your 'fact' function? I was assuming
something along those lines:

  fun fact :: "nat => nat" where
  "fact 0 = 1" |
  "fact (Suc n) = (Suc n) * fact n"





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