Intuitionistic principles in Coq

I formalized some of the notions that were presented in a course on intuitionistic mathematics by W. Veldman (Radboud).

Name		Name	Last commit message	Last commit date
Latest commit History 84 Commits
doc		doc
.gitignore		.gitignore
README.md		README.md
_CoqProject		_CoqProject
bar.v		bar.v
bcp.v		bcp.v
bks.v		bks.v
choice.v		choice.v
classic.v		classic.v
fan.v		fan.v
faninj.v		faninj.v
func.v		func.v
kleene.v		kleene.v
lib.v		lib.v
reals.v		reals.v
seq.v		seq.v
set.v		set.v
spr.v		spr.v
tau.v		tau.v

Provide feedback