IntensionalEquality

Pierre Letouzey edited this page Oct 27, 2017 · 6 revisions

Intensional Equality

Why Have Intensional Equality

Suppose you create a countable data type of recursive functions, RecursiveFunction, along with some execution function exec : forall (rf:RecursiveFunction) (input:N) (steps:N) : option N, then you could add an axiom

reflect : forall (f:N -> N),
 {rf:RecursiveFunction
 | forall (n m:N) {(exec rf n m)=Some (f n)}+{(exec rf n m)=None}

During ProgramExtraction this function could be mapped to a function satisfying this signature. This might be a useful thing to do.

I think that if Coq had extensional equality of functions, such an axiom could not be mapped to any function during program extraction.

Clone this wiki locally
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.
Press h to open a hovercard with more details.