Pinned Loading
-
-
-
-
Coq Gallina: pattern match vs elimin...
Coq Gallina: pattern match vs eliminator 1(*
23equality in stdlib:
4https://coq.inria.fr/doc/V8.18.0/refman/proofs/writing-proofs/equality.html
5 -
Coq Proof: 0 = 1 -> 0 = 1 + n
Coq Proof: 0 = 1 -> 0 = 1 + n 1(* https://www.cs.cornell.edu/courses/cs3110/2018sp/a5/coq-tactics-cheatsheet.html *)
23Definition ex0 :
4forall n : nat,
50 = 1 -> 0 = 1 + n
Something went wrong, please refresh the page to try again.
If the problem persists, check the GitHub status page or contact support.
If the problem persists, check the GitHub status page or contact support.