[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: inst? and overloaded operators
> could have also checked the intval_adt.pvs file and applied the
> axioms in there manually).
I did, but I only found extensionality which goes the opposite
direction. Am I overlooking something?
You can use intval_v_intval twice to prove injectiveness. I.e., you
(INST - "x1!1")
(INST - "x2!1")
(REPLACE -5 *)