[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: beginner's problem




But when I added this theorem...

   fact_thm4: THEOREM (FORALL (m:nat): factorial(m) = fact_loop(m, 1))
                                                      ^^^^^^^^^

Steve,

You just misspelt fac_loop as fact_loop.  PVS's error message in this
situation could be more illuminating.  But "no resolution" means
it is not defined.

- Srivas