Index
| $$ | Logic.Proof, GDP |
| $: | Data.Refined, GDP |
| && | Logic.Propositional, GDP |
| --> | Logic.Propositional, GDP |
| ... | Data.Refined, GDP |
| ...> | Data.Refined, GDP |
| ...? | Data.Refined, GDP |
| /\ | Logic.Propositional, GDP |
| ::: | Data.Refined, GDP |
| == | Theory.Equality, GDP |
| ==. | Theory.Equality, GDP |
| ? | Data.Refined, GDP |
| absurd | Logic.Propositional, GDP |
| And | Logic.Propositional, GDP |
| and_elim | Logic.Propositional, GDP |
| and_elimL | Logic.Propositional, GDP |
| and_elimR | Logic.Propositional, GDP |
| and_intro | Logic.Propositional, GDP |
| and_map | Logic.Propositional, GDP |
| and_mapL | Logic.Propositional, GDP |
| and_mapR | Logic.Propositional, GDP |
| Antisymmetric | Logic.NegClasses, GDP |
| antisymmetric | Logic.NegClasses, GDP |
| apply | Theory.Equality, GDP |
| Arg | |
| 1 (Type/Class) | Data.Arguments, GDP |
| 2 (Data Constructor) | Data.Arguments, GDP |
| arg | Data.Arguments, GDP |
| Argument | Data.Arguments, GDP |
| assert | Data.Refined, GDP |
| Associative | Logic.Classes, GDP |
| associative | Logic.Classes, GDP |
| axiom | Logic.Proof, GDP |
| Classical | Logic.Propositional, GDP |
| classically | Logic.Propositional, GDP |
| Commutative | Logic.Classes, GDP |
| commutative | Logic.Classes, GDP |
| conjure | Data.Refined, GDP |
| contradiction | Logic.Propositional, GDP |
| contradicts | Logic.Propositional, GDP |
| contradicts' | Logic.Propositional, GDP |
| contrapositive | Logic.Propositional, GDP |
| Defining | Theory.Named, GDP |
| Defn | Theory.Named, GDP |
| defn | Theory.Named, GDP |
| DistributiveL | Logic.Classes, GDP |
| distributiveL | Logic.Classes, GDP |
| DistributiveR | Logic.Classes, GDP |
| distributiveR | Logic.Classes, GDP |
| elim_inj | Logic.Classes, GDP |
| Equals | Theory.Equality, GDP |
| Exists | Logic.Propositional, GDP |
| exorcise | Data.Refined, GDP |
| ex_elim | Logic.Propositional, GDP |
| ex_intro | Logic.Propositional, GDP |
| FALSE | Logic.Propositional, GDP |
| ForAll | Logic.Propositional, GDP |
| forP | Data.Refined, GDP |
| forP_ | Data.Refined, GDP |
| GetArg | Data.Arguments, GDP |
| given | Logic.Proof, GDP |
| Idempotent | Logic.Classes, GDP |
| idempotent | Logic.Classes, GDP |
| Implies | Logic.Propositional, GDP |
| impl_elim | Logic.Propositional, GDP |
| impl_intro | Logic.Propositional, GDP |
| impl_map | Logic.Propositional, GDP |
| impl_mapL | Logic.Propositional, GDP |
| impl_mapR | Logic.Propositional, GDP |
| Injective | Logic.Classes, GDP |
| irrefl | Logic.NegClasses, GDP |
| Irreflexive | Logic.NegClasses, GDP |
| lem | Logic.Propositional, GDP |
| LHS | Data.Arguments, GDP |
| modus_ponens | Logic.Propositional, GDP |
| modus_tollens | Logic.Propositional, GDP |
| name | Theory.Named, GDP |
| name2 | Theory.Named, GDP |
| name3 | Theory.Named, GDP |
| Named | Theory.Named, GDP |
| noncontra | Logic.Propositional, GDP |
| Not | Logic.Propositional, GDP |
| not_intro | Logic.Propositional, GDP |
| not_map | Logic.Propositional, GDP |
| not_not_elim | Logic.Propositional, GDP |
| Or | Logic.Propositional, GDP |
| or_elim | Logic.Propositional, GDP |
| or_elimL | Logic.Propositional, GDP |
| or_elimR | Logic.Propositional, GDP |
| or_introL | Logic.Propositional, GDP |
| or_introR | Logic.Propositional, GDP |
| or_map | Logic.Propositional, GDP |
| or_mapL | Logic.Propositional, GDP |
| or_mapR | Logic.Propositional, GDP |
| Proof | Logic.Proof, GDP |
| propEq | Theory.Equality, GDP |
| refl | Logic.Classes, GDP |
| reflectEq | Theory.Equality, GDP |
| Reflexive | Logic.Classes, GDP |
| rename | Data.Refined, GDP |
| RHS | Data.Arguments, GDP |
| same | Theory.Equality, GDP |
| Satisfies | Data.Refined, GDP |
| SetArg | Data.Arguments, GDP |
| sorry | Logic.Proof, GDP |
| substitute | Theory.Equality, GDP |
| substituteL | Theory.Equality, GDP |
| substituteR | Theory.Equality, GDP |
| Symmetric | Logic.Classes, GDP |
| symmetric | Logic.Classes, GDP |
| The | |
| 1 (Type/Class) | Data.The, GDP |
| 2 (Data Constructor) | Data.The, GDP |
| the | Data.The, GDP |
| Transitive | Logic.Classes, GDP |
| transitive | Logic.Classes, GDP |
| transitive' | Logic.Classes, GDP |
| traverseP | Data.Refined, GDP |
| traverseP_ | Data.Refined, GDP |
| TRUE | Logic.Propositional, GDP |
| true | Logic.Propositional, GDP |
| univ_elim | Logic.Propositional, GDP |
| univ_intro | Logic.Propositional, GDP |
| unname | Data.Refined, GDP |
| \/ | Logic.Propositional, GDP |
| |$ | Logic.Proof, GDP |
| |. | Logic.Proof, GDP |
| |/ | Logic.Proof, GDP |
| |\ | Logic.Proof, GDP |
| || | Logic.Propositional, GDP |
| ~~ | Theory.Named, GDP |
| ∧ | Logic.Propositional, GDP |
| ∨ | Logic.Propositional, GDP |