Coq tactics to simplify inequality proofs
Interval provides vernacular files containing tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant.
System | Target | Derivation | Build status |
---|---|---|---|
x86_64-linux | /gnu/store/jhr4y2irdmjbcm538z3zs1gzp4klifp0-coq-interval-4.3.0.drv | ||
powerpc64le-linux | /gnu/store/1byng5dbhgs0f07gbkiy5nza5npxvs10-coq-interval-4.3.0.drv | ||
mips64el-linux | /gnu/store/2jxax7xa69yab0cd994xlnmbjsn0pir6-coq-interval-4.3.0.drv | ||
i686-linux | /gnu/store/i784q32xzv7qjhddf74dhgfdxqsb7bk6-coq-interval-4.3.0.drv | ||
i586-gnu | /gnu/store/1a1f3swi7xw9a6ypgs8f003rq29q2l1k-coq-interval-4.3.0.drv | ||
armhf-linux | /gnu/store/5gn9hlgr29dqaz31s58nyq3qsaadv3yi-coq-interval-4.3.0.drv | ||
aarch64-linux | /gnu/store/3bjdkk7j93qr3q0khzl8fv9s21ka1cq7-coq-interval-4.3.0.drv |
Linter | Message | Location |
---|---|---|
optional-tests Make sure tests are only run when requested | the 'check' phase should respect #:tests? |