Skip to main content
Technical

Using Coq in the browser: jsCoq

— Hans-Dieter Hiep

In this blog post, I will try embedding Coq in the browser using jsCoq (work in progress).

Require Import Classical.

Proposition test (A B: Prop): A \/ B -> ((A -> B) -> B).
  (* Complete the proof here. *)
Admitted.

Testing out how the side-panel moves when the content becomes longer.

Proposition test2 (A B: Prop): A /\ B -> A \/ B.
  (* Complete the proof here. *)
Admitted.

Test.

Proposition test3 (A B: Prop): A \/ B -> ~(~A /\ ~B).
  (* Complete the proof here. *)
Admitted.

Another test. With some mathematics inside \[f(x) = x + 2\] which is in display-style.

Require Import ZArith Psatz.
Open Scope Z_scope.
Proposition test (f: Z -> Z) (x: Z): f x = f x + 2.
Admitted.

More tests.