false.v « coqwc « test-suite - debian-coq - Debian packaging for Coq

summary refs log tree commit diff

path: root/test-suite/coqwc/false.v

blob: 640f9ea7f092de5a21bd5810898b2f224644603b (plain)

Axiom x : nat.

Definition foo (x : nat) := x + 1.

Lemma bar : False.
 idtac.
 idtac. (* truth is overrated *)
Admitted.