Rocq Comparator

Challenge challenge.v

Solution solution.v

waiting for the Rocq runtime to load…

Advanced options

Theorem names (override) comma/space separated; leave blank to auto-detect Theorem/Lemma/Example… declarations in the challenge

Definition names (holes) definitions the challenge leaves as holes for the solution to fill

Top (library name) logical name coqdep would derive for challenge.v (blank = derived)

Timeout (seconds)

Permitted axioms fully-qualified kernel names or Prefix.* wildcards (comma/space separated)

Trust challenge-declared axiomsParameters/Axioms/Admitted helpers the challenge itself declares are auto-permitted, pinned to their challenge type -noinit (skip the Corelib prelude)check it only for a prelude-free core-Gallina check: no nat, no notations, no tactics beyond the kernel primitives -impredicative-setmake Set impredicative, as in early Coq: a type in Set may quantify over all of Set. Changes the logic (inconsistent with some classical axioms). Only for challenges written for it. -indices-matteran inductive type must live in a universe at least as large as its indices (the rule used by homotopy type theory). The bundled libraries were compiled without it, so it only fits challenges that avoid them.

No verdict yet. Edit the two proofs above and click Run.

A real Rocq 9.2 kernel (a wasm_of_ocaml build of rocq-runtime and rocq-comparator) runs in a Web Worker in your browser; no source leaves your machine. Prototype produced by Claude Fable 5.1, inspired by the Lean comparator. Source: rocq-comparator-web, rocq-comparator.