hout-0.1.0.0: Non-interactive proof assistant monad for first-order logic. (Index)

hout-0.1.0.0: Non-interactive proof assistant monad for first-order logic.

Index

/\	Hout.Logic.Intuitionistic
<->	Hout.Logic.Intuitionistic
admitted	Hout.Prover.Proofs
andElimLeft	Hout.Logic.Intuitionistic
andElimRight	Hout.Logic.Intuitionistic
andIntro	Hout.Logic.Intuitionistic
apply	Hout.Prover.Tactics
applyF	Hout.Prover.Tactics
applyH	Hout.Prover.Tactics
assert	Hout.Prover.Tactics
Axiom	Hout.Prover.Proofs
bindH	Hout.Prover.Tactics
combineH	Hout.Prover.Tactics
ConstraintWitness	Hout.Logic.FirstOrder
Corollary	Hout.Prover.Proofs
DataKindWitness	Hout.Logic.FirstOrder
Definition	Hout.Prover.Proofs
enough	Hout.Prover.Tactics
eqRefl	Hout.Logic.FirstOrder
eqRewrite	Hout.Logic.FirstOrder
eqSym	Hout.Logic.FirstOrder
eqTrans	Hout.Logic.FirstOrder
Equal	Hout.Logic.FirstOrder
exact	Hout.Prover.Tactics
Example	Hout.Prover.Proofs
exFalso	Hout.Logic.Intuitionistic
Exists
1 (Type/Class)	Hout.Logic.FirstOrder
2 (Data Constructor)	Hout.Logic.FirstOrder
exists	Hout.Prover.Tactics
existsElim	Hout.Logic.FirstOrder
existsIntro	Hout.Logic.FirstOrder
False	Hout.Logic.Intuitionistic
Forall
1 (Type/Class)	Hout.Logic.FirstOrder
2 (Data Constructor)	Hout.Logic.FirstOrder
forallElim	Hout.Logic.FirstOrder
forallIntro	Hout.Logic.FirstOrder
generalize	Hout.Prover.Tactics
iffElimLeft	Hout.Logic.Intuitionistic
iffElimRight	Hout.Logic.Intuitionistic
iffIntro	Hout.Logic.Intuitionistic
intro	Hout.Prover.Tactics
left	Hout.Prover.Tactics
Lemma	Hout.Prover.Proofs
name	Hout.Prover.Tactics
noncomputable	Hout.Prover.Proofs
Not	Hout.Logic.Intuitionistic
orElim	Hout.Logic.Intuitionistic
orIntroLeft	Hout.Logic.Intuitionistic
orIntroRight	Hout.Logic.Intuitionistic
Proof	Hout.Prover.Proofs
qed	Hout.Prover.Tactics
Refl	Hout.Logic.FirstOrder
reflexivity	Hout.Prover.Tactics
rewrite	Hout.Prover.Tactics
rewriteRev	Hout.Prover.Tactics
right	Hout.Prover.Tactics
runProof	Hout.Prover.Proofs
split	Hout.Prover.Tactics
symmetry	Hout.Prover.Tactics
Tactic
1 (Type/Class)	Hout.Prover.Tactics
2 (Data Constructor)	Hout.Prover.Tactics
Theorem	Hout.Prover.Proofs
transitivity	Hout.Prover.Tactics
True	Hout.Logic.Intuitionistic
trueIntro	Hout.Logic.Intuitionistic
Witness
1 (Type/Class)	Hout.Logic.FirstOrder
2 (Data Constructor)	Hout.Logic.FirstOrder
\/	Hout.Logic.Intuitionistic