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.
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.