Stream: Coq users

Topic: Basic integration


view this post on Zulip Anders Larsson (Sep 08 2022 at 14:32):

What is currently the best way to prove simple integrals in Coq? I guess it could be done in math-comp analysis and there seem to be some older libraries too. There are two unsolved problems on Freeks 100-list that i guess is boils down to simple integrals.

view this post on Zulip Karl Palmskog (Sep 08 2022 at 14:39):

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (coq-num-analysis package in Coq opam)

view this post on Zulip Anders Larsson (Sep 08 2022 at 14:55):

Karl Palmskog said:

one recent library on integration: https://depot.lipn.univ-paris13.fr/mayero/coq-num-analysis/ (coq-num-analysis package in Coq opam)

Nice. I'll have a look. (opam installation failed but that can probably be solved).

$ opam search coq-num-analysis
# Packages matching: match(*coq-num-analysis*)
# No matches found

view this post on Zulip Karl Palmskog (Sep 08 2022 at 15:05):

you need to do opam update, then opam show coq-num-analysis.1.0.0 works

view this post on Zulip Karl Palmskog (Sep 08 2022 at 15:07):

and also make sure to add Coq opam released repo as here: https://github.com/coq/opam-coq-archive#usage


Last updated: Jan 28 2023 at 07:30 UTC