Skip to content

clarus/falso

Folders and files

NameName
Last commit message
Last commit date

Latest commit

Mar 24, 2015
319e74a · Mar 24, 2015

History

5 Commits
Mar 24, 2015
Mar 24, 2015
Mar 24, 2015
Mar 24, 2015
Mar 24, 2015
Mar 24, 2015

Repository files navigation

Falso

A proof of false.

This is an implementation in Coq of the Falso proof system.

Use

Install with OPAM for Coq:

opam repo add coq-stable https://github.com/coq/repo-stable.git
opam install coq:falso

In a tedious development:

Require Import Falso.All.

Lemma hard : forall (A : Prop), A.
  destruct falso.
Qed.

Print Assumptions hard.

About

A proof of false in Coq.

Resources

License

Stars

Watchers

Forks

Packages

No packages published