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/ivcdnr0dlbdx0m4a2vxx2k380y24y70x-coq-interval-3.4.1.drv | ||
| mips64el-linux | /gnu/store/8kg5nky8pijnzv86ss78mc1gjsl69cjk-coq-interval-3.4.1.drv | ||
| i686-linux | /gnu/store/mdzp62vh2x8fg1hqp6lrvprwf7mjm4ng-coq-interval-3.4.1.drv | ||
| armhf-linux | /gnu/store/71c4msqlzv2a4zg1b482w1irkgyjd9p1-coq-interval-3.4.1.drv | ||
| aarch64-linux | /gnu/store/a0b1rhxxwjgrb051bg6sg5bm7bjz5rig-coq-interval-3.4.1.drv |
| Linter | Message | Location |
|---|---|---|
| derivation Report failure to compile a package to a derivation | failed to create x86_64-linux derivation: path ‘/gnu/store/1dz7hwpizsbvz88j1g2s4c16ayjy36dz-coq-8.10.2.drv’ is not valid | |
| derivation Report failure to compile a package to a derivation | failed to create i686-linux derivation: path ‘/gnu/store/imq41gd3q2767il9gq6mqh5cv44x09rf-guile-2.2.6.drv’ is not valid | |
| derivation Report failure to compile a package to a derivation | failed to create armhf-linux derivation: path ‘/gnu/store/9wn798a6w534mnn4f28lglbjmib9n392-zlib-1.2.11.drv’ is not valid | |
| derivation Report failure to compile a package to a derivation | failed to create aarch64-linux derivation: path ‘/gnu/store/0afbxr7962z9ci6kw840n088qsmyz8lr-guile-2.2.6.drv’ is not valid | |
| derivation Report failure to compile a package to a derivation | failed to create mips64el-linux derivation: path ‘/gnu/store/aiwgcl5dppar2s8l408bshywjybsy3nd-zlib-1.2.11.drv’ is not valid |