Index
| $: | 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 |
| 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 |
| bimapAnd | Logic.Propositional, GDP |
| bimapOr | Logic.Propositional, GDP |
| Classical | Logic.Propositional, GDP |
| classically | Logic.Propositional, GDP |
| classify | Theory.Lists |
| classify' | Theory.Lists |
| Commutative | Logic.Classes, GDP |
| commutative | Logic.Classes, GDP |
| conjure | Data.Refined, GDP |
| Cons | Theory.Lists |
| cons | Theory.Lists |
| Cons' | Theory.Lists |
| consIsCons | Theory.Lists |
| consIsList | Theory.Lists |
| Cons_ | Theory.Lists |
| 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 |
| dimapImpl | Logic.Propositional, GDP |
| DistributiveL | Logic.Classes, GDP |
| distributiveL | Logic.Classes, GDP |
| DistributiveR | Logic.Classes, GDP |
| distributiveR | Logic.Classes, GDP |
| elimAndL | Logic.Propositional, GDP |
| elimAndR | Logic.Propositional, GDP |
| elimEx | Logic.Propositional, GDP |
| elimImpl | Logic.Propositional, GDP |
| elimNot | Logic.Propositional, GDP |
| elimNotNot | Logic.Propositional, GDP |
| elimOr | Logic.Propositional, GDP |
| elimOrL | Logic.Propositional, GDP |
| elimOrR | Logic.Propositional, GDP |
| elimUniv | Logic.Propositional, GDP |
| elim_inj | Logic.Classes, GDP |
| Equals | Theory.Equality, GDP |
| Exists | Logic.Propositional, GDP |
| exorcise | Data.Refined, GDP |
| Fact | Logic.Implicit, GDP |
| FALSE | Logic.Propositional, GDP |
| firstAnd | Logic.Propositional, GDP |
| firstOr | Logic.Propositional, GDP |
| ForAll | Logic.Propositional, GDP |
| forP | Data.Refined, GDP |
| forP_ | Data.Refined, GDP |
| GetArg | Data.Arguments, GDP |
| Head | Theory.Lists |
| head | Theory.Lists |
| headOfCons | Theory.Lists |
| Idempotent | Logic.Classes, GDP |
| idempotent | Logic.Classes, GDP |
| Implies | Logic.Propositional, GDP |
| Injective | Logic.Classes, GDP |
| introAnd | Logic.Propositional, GDP |
| introAnd' | Logic.Propositional, GDP |
| introEx | Logic.Propositional, GDP |
| introImpl | Logic.Propositional, GDP |
| introNot | Logic.Propositional, GDP |
| introOrL | Logic.Propositional, GDP |
| introOrR | Logic.Propositional, GDP |
| introUniv | Logic.Propositional, GDP |
| irrefl | Logic.NegClasses, GDP |
| Irreflexive | Logic.NegClasses, GDP |
| IsCons | |
| 1 (Type/Class) | Theory.Lists |
| 2 (Data Constructor) | Theory.Lists |
| IsCons_ | Theory.Lists |
| IsList | Theory.Lists |
| IsNil | |
| 1 (Type/Class) | Theory.Lists |
| 2 (Data Constructor) | Theory.Lists |
| IsNil_ | Theory.Lists |
| known | Logic.Implicit, GDP |
| lem | Logic.Propositional, GDP |
| LHS | Data.Arguments, GDP |
| ListCase | Theory.Lists |
| ListCase' | Theory.Lists |
| listInduction | Theory.Lists |
| listIsList | Theory.Lists |
| listShapes | Theory.Lists |
| lmapImpl | Logic.Propositional, GDP |
| mapNot | Logic.Propositional, GDP |
| modusPonens | Logic.Propositional, GDP |
| modusTollens | Logic.Propositional, GDP |
| name | Theory.Named, GDP |
| name2 | Theory.Named, GDP |
| name3 | Theory.Named, GDP |
| Named | Theory.Named, GDP |
| Nil | Theory.Lists |
| nil | Theory.Lists |
| Nil' | Theory.Lists |
| nilIsList | Theory.Lists |
| Nil_ | Theory.Lists |
| noncontra | Logic.Propositional, GDP |
| Not | Logic.Propositional, GDP |
| note | Logic.Implicit, GDP |
| on | Logic.Implicit, GDP |
| Or | 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 |
| rmapImpl | Logic.Propositional, GDP |
| same | Theory.Equality, GDP |
| Satisfies | Data.Refined, GDP |
| secondAnd | Logic.Propositional, GDP |
| secondOr | Logic.Propositional, 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 |
| Tail | Theory.Lists |
| tail | Theory.Lists |
| tailOfCons | Theory.Lists |
| 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 |
| unname | Data.Refined, GDP |
| \/ | Logic.Propositional, GDP |
| || | Logic.Propositional, GDP |
| ~~ | Theory.Named, GDP |
| ∧ | Logic.Propositional, GDP |
| ∨ | Logic.Propositional, GDP |