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
I believe we made those proofs computational in
Thanks. I can't find any concrete implementation, maybe it's in CoRN?
Found it. TIL about
I expect there are similar lemmas in the reals/fast and reals/faster directories.
Last updated: Oct 04 2023 at 23:01 UTC