Hello Ramana.
On 05/10/17 19:18, Ramana Kumar wrote:
> My intuition says that working with total functions (and especially
> predicates) will be easier.
> Why? I don't know exactly, but here are some possible reasons:
> you can just use plain rewriting rather than conditional rewriting,
> and you
My intuition says that working with total functions (and especially
predicates) will be easier.
Why? I don't know exactly, but here are some possible reasons:
you can just use plain rewriting rather than conditional rewriting,
and you don't need to state so many assumptions explicitly on your
Hello.
What is the preferred way to define functions only for some values? For
example, as in arithmetic$DIV in HOL?:
⊢ ∀n. 0 < n ⇒ ∀k. k = k DIV n * n + k MOD n ∧ k MOD n < n)
Here nothing is asserted for the value of DIV for n = 0, thus it is
“undefined” in some sense. I know that this can
