Hi,

I'm a bit new to Coq. I'd like to build an interactive demo of what a continuity proof computes. `continuity_pt_plus`

from the Reals builtin library returns a `Prop`

, so I can't extract a function that would graph it in a hypothetical js_of_ocaml demo. I've re-implemented a monolithic proof of additivity (?) but I was wondering whether I could slightly adapt the existing library to use `sig`

.

Thanks!

I believe we made those proofs computational in

https://github.com/coq-community/math-classes

Thanks. I can't find any concrete implementation, maybe it's in CoRN?

Found it. TIL about `CProp`

...

I expect there are similar lemmas in the reals/fast and reals/faster directories.

Last updated: Jan 27 2023 at 00:03 UTC