Mode | Name | Size | |
---|---|---|---|
-rw-r--r-- | Consequences.agda | 5496 | logplain |
d--------- | Construct | 446 | logplain |
-rw-r--r-- | Core.agda | 6264 | logplain |
-rw-r--r-- | EqReasoning.agda | 946 | logplain |
-rw-r--r-- | EquivalenceClosure.agda | 451 | logplain |
-rw-r--r-- | HeterogeneousEquality.agda | 10863 | logplain |
d--------- | HeterogeneousEquality | 115 | logplain |
d--------- | Indexed | 168 | logplain |
-rw-r--r-- | Lattice.agda | 17073 | logplain |
d--------- | List | 129 | logplain |
-rw-r--r-- | OrderMorphism.agda | 1627 | logplain |
-rw-r--r-- | PartialOrderReasoning.agda | 511 | logplain |
-rw-r--r-- | PreorderReasoning.agda | 1909 | logplain |
d--------- | Product | 129 | logplain |
d--------- | Properties | 613 | logplain |
-rw-r--r-- | PropositionalEquality.agda | 7117 | logplain |
d--------- | PropositionalEquality | 77 | logplain |
-rw-r--r-- | Reflection.agda | 3932 | logplain |
-rw-r--r-- | SetoidReasoning.agda | 1511 | logplain |
d--------- | Sigma | 42 | logplain |
-rw-r--r-- | StrictPartialOrderReasoning.agda | 726 | logplain |
-rw-r--r-- | Sum.agda | 1429 | logplain |
-rw-r--r-- | SymmetricClosure.agda | 443 | logplain |
d--------- | Vec | 42 | logplain |