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/0zxhac4v0860xjs6brir7x1a3hd4iqak-coq-interval-4.3.0.drv | ||
powerpc64le-linux | /gnu/store/y0gh35703s4nkzg1nbxkh2939n5y08nh-coq-interval-4.3.0.drv | ||
mips64el-linux | /gnu/store/6ggdq4ckckirzgzg3965mxjzdkjs5sc3-coq-interval-4.3.0.drv | ||
i686-linux | /gnu/store/w5j5hc00hih1bjkq0acwf2d84nx58m88-coq-interval-4.3.0.drv | ||
i586-gnu | /gnu/store/2y0nlwiswb9rgji9pmzxah288h1zdfvb-coq-interval-4.3.0.drv | ||
armhf-linux | /gnu/store/x8yh3ihwh3kl513r9pdsxdfwzs953kva-coq-interval-4.3.0.drv | ||
aarch64-linux | /gnu/store/h2j1g0v48zbi3nwq7vrmxw2285jg73g9-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? |