TypeClasses.lean`

148 declarations, 0 contain sorry, 0 declared as axioms

Imports (2)

VersoManual
TPiL.Examples

structure Ex.Add line 23 source
Source comment
----
Distinct definitions of this name: examples/Examples/InteractExample3g3kno8ekkpr.lean:2 (different declaration text), examples/Examples/InteractExamplextkkn9qu4li2b.lean:2 (same statement text; different proof or body). Qualify references as Ex.Add@path.
```
structure Add (α : Type) where
…
```
Mentions: α
structure Ex.Add line 35 source
Distinct definitions of this name: examples/Examples/InteractExample3g3kno8ekkpr.lean:2 (different declaration text), examples/Examples/InteractExamplextkkn9qu4li2b.lean:2 (same declaration text). Qualify references as Ex.Add@path.
def Ex.double line 37 source
Distinct definitions of this name: examples/Examples/InteractExamplextkkn9qu4li2b.lean:4 (same statement text; different proof or body). Qualify references as Ex.double@path.
structure Ex.Ex.Add line 50 source
def Ex.Ex.double line 53 source
Source comment
----
```
def double (s : Add α) (x : α) : α :=
…
```
Mentions: Ex.Ex.s, Ex.Ex.Add, α, x
class Ex.Ex.Add line 82 source
Source comment
----
```
class Add (α : Type) where
…
```
Mentions: α
class Ex.Ex.Add line 98 source
instance Ex.Ex.(instance at line 101) line 101 source
Source comment
----
```
instance : Add Nat where
…
```
Mentions: Ex.Ex.Add
instance Ex.Ex.(instance at line 104) line 104 source
instance Ex.Ex.(instance at line 107) line 107 source
class Ex.Ex.Add line 117 source
instance Ex.Ex.(instance at line 120) line 120 source
Source comment
----
```
instance : Add Nat where
…
```
Mentions: Ex.Ex.Add
instance Ex.Ex.(instance at line 123) line 123 source
instance Ex.Ex.(instance at line 126) line 126 source
class Ex.Ex.Ex.Add line 138 source
instance Ex.Ex.Ex.(instance at line 140) line 140 source
instance Ex.Ex.Ex.(instance at line 142) line 142 source
instance Ex.Ex.Ex.(instance at line 144) line 144 source
def Ex.Ex.Ex.double line 147 source
Source comment
----
```
def double [Add α] (x : α) : α :=
…
```
Mentions: Ex.Ex.Ex.Add, α, x
instance Ex.Ex.(instance at line 171) line 171 source
def Ex.Ex.head line 185 source
class Ex.Ex.Ex.Inhabited line 205 source
Source comment
----
```
class Inhabited (α : Type u) where
…
```
Mentions: α
class Ex.Ex.Ex.Inhabited line 222 source
instance Ex.Ex.Ex.(instance at line 225) line 225 source
Source comment
----
```
instance : Inhabited Bool where
…
```
Mentions: Ex.Ex.Ex.Inhabited
instance Ex.Ex.Ex.(instance at line 228) line 228 source
instance Ex.Ex.Ex.(instance at line 231) line 231 source
instance Ex.Ex.Ex.(instance at line 234) line 234 source
class Ex.Ex.Ex.Inhabited line 248 source
instance Ex.Ex.Ex.(instance at line 250) line 250 source
instance Ex.Ex.Ex.(instance at line 252) line 252 source
instance Ex.Ex.Ex.(instance at line 254) line 254 source
instance Ex.Ex.Ex.(instance at line 256) line 256 source
instance Ex.Ex.(instance at line 283) line 283 source
class Ex.Ex.Ex.Inhabited line 292 source
instance Ex.Ex.Ex.(instance at line 294) line 294 source
instance Ex.Ex.Ex.(instance at line 296) line 296 source
opaque Ex.Ex.Ex.default line 298 source
instance Ex.Ex.Ex.(instance at line 301) line 301 source
Source comment
----
```
instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
…
```
Mentions: Ex.Ex.Ex.Inhabited, α, β
instance Ex.Ex.(instance at line 312) line 312 source
def Ex.Ex.foo line 330 source
theorem Ex.Ex.ex line 333 source
structure Ex.Ex.Person line 359 source
instance Ex.Ex.(instance at line 363) line 363 source
structure Ex.Ex.Rational line 381 source
instance Ex.Ex.(instance at line 386) line 386 source
instance Ex.Ex.(instance at line 389) line 389 source
structure Ex.Ex.Rational line 401 source
instance Ex.Ex.(instance at line 406) line 406 source
instance Ex.Ex.(instance at line 409) line 409 source
class Ex.Ex.Monoid line 429 source
instance Ex.Ex.(instance at line 433) line 433 source
def Ex.Ex.getUnit line 436 source

class Ex.Ex.Ex.HMul line 474 source

Source comment

----

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
…

Mentions: α, β

instance Ex.Ex.Ex.(instance at line 479) line 479 source
instance Ex.Ex.Ex.(instance at line 482) line 482 source

class Ex.Ex.Ex.HMul line 502 source

Source comment

----

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
…

Mentions: α, β

instance Ex.Ex.Ex.(instance at line 507) line 507 source
instance Ex.Ex.Ex.(instance at line 510) line 510 source
instance Ex.Ex.Ex.(instance at line 513) line 513 source

class Ex.Ex.Ex.HMul line 555 source

Source comment

----

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
…

Mentions: α, β

instance Ex.Ex.Ex.(instance at line 560) line 560 source
def Ex.Ex.Ex.xs line 563 source

class Ex.Ex.Ex.HMul line 586 source

Source comment

----

class HMul (α : Type u) (β : Type v) (γ : outParam (Type w)) where
…

Mentions: α, β

instance Ex.Ex.Ex.(instance at line 592) line 592 source
def Ex.Ex.Ex.xs line 595 source
structure Ex.Ex.Rational line 616 source
instance Ex.Ex.(instance at line 622) line 622 source
instance Ex.Ex.(instance at line 625) line 625 source
class Ex.Ex.Ex.OfNat line 645 source
Source comment
----
```
class OfNat (α : Type u) (n : Nat) where
…
```
Mentions: α, n
instance Ex.Ex.Ex.(instance at line 649) line 649 source
class Ex.Ex.Ex.HMul line 652 source
class Ex.Ex.Ex.Mul line 655 source
instance Ex.Ex.Ex.(instance at line 659) line 659 source
structure Ex.Ex.Point line 680 source
def Ex.Ex.double line 689 source
def Ex.Ex.triple line 701 source
structure Ex.Ex.Point line 710 source
instance Ex.Ex.addPoint line 714 source
def Ex.Ex.double line 717 source
def Ex.Ex.triple line 729 source
structure Ex.Ex.Point line 744 source
def Ex.Ex.Point.double line 753 source
structure Ex.Ex.Point line 782 source
def Ex.Ex.Point.double line 791 source
class inductive Ex.Ex.Hidden.Decidable line 830 source
Source comment
----
```
class inductive Decidable (p : Prop) where
…
```
example Ex.Ex.(example at line 845) line 845 source
def Ex.Ex.Hidden.ite line 852 source
Source comment
----
```
def ite {α : Sort u}
    (c : Prop) [h : Decidable c]
    (t e : α) : α :=
…
```
Mentions: α, Ex.Ex.Hidden.Decidable, t

def Ex.Ex.Hidden.dite line 868 source

Source comment

----

def dite {α : Sort u}
    (c : Prop) [h : Decidable c]
    (t : c → α) (e : Not c → α) : α :=
…

Mentions: α, Ex.Ex.Hidden.Decidable, t

example Ex.Ex.(example at line 882) line 882 source
def Ex.Ex.step line 909 source
instance Ex.Ex.of line 922 source
instance Ex.Ex.Hidden.(instance at line 948) line 948 source
example Ex.Ex.(example at line 967) line 967 source
example Ex.Ex.(example at line 970) line 970 source
example Ex.Ex.(example at line 973) line 973 source
theorem Ex.Ex.ex line 976 source
def Ex.Ex.foo line 1012 source
def Ex.Ex.bar line 1013 source
def Ex.Ex.Set line 1038 source
example Ex.Ex.(example at line 1047) line 1047 source
instance Ex.Ex.(instance at line 1050) line 1050 source
class Ex.Ex.Foo line 1100 source
instance Ex.Ex.(instance at line 1104) line 1104 source
instance Ex.Ex.i2 line 1108 source
example Ex.Ex.(example at line 1112) line 1112 source
instance Ex.Ex.(instance at line 1115) line 1115 source
example Ex.Ex.(example at line 1119) line 1119 source
def Ex.Ex.Set line 1131 source
instance Ex.Ex.(instance at line 1154) line 1154 source
def Ex.Ex.Set line 1171 source
def Ex.Ex.Set.empty line 1172 source
def Ex.Ex.Set.mem line 1173 source
def Ex.Ex.Set.singleton line 1174 source
def Ex.Ex.Set.union line 1175 source
def Ex.Ex.List.toSet line 1179 source
Source comment
----
```
def List.toSet : List α → Set α
  | []    => Set.empty
  | a::as => {a} ∪ as.toSet
```
Mentions: α, Ex.Ex.Set, Ex.Ex.Set.empty, as
instance Ex.Ex.(instance at line 1183) line 1183 source
def Ex.Ex.s line 1186 source
def Ex.Ex.Set line 1195 source
def Ex.Ex.Set.empty line 1196 source
def Ex.Ex.Set.mem line 1197 source
def Ex.Ex.Set.singleton line 1198 source
def Ex.Ex.Set.union line 1199 source
def Ex.Ex.List.toSet line 1202 source
instance Ex.Ex.(instance at line 1205) line 1205 source
def Ex.Ex.s line 1208 source
Source comment
----
```
def s : Set Nat := {1}
…
```
Mentions: Ex.Ex.Set
instance Ex.Ex.(instance at line 1219) line 1219 source
structure Ex.Ex.Semigroup line 1234 source
instance Ex.Ex.(instance at line 1239) line 1239 source
structure Ex.Ex.Semigroup line 1246 source
instance Ex.Ex.(instance at line 1251) line 1251 source
instance Ex.Ex.(instance at line 1256) line 1256 source
structure Ex.Ex.Semigroup line 1263 source
instance Ex.Ex.(instance at line 1267) line 1267 source
structure Ex.Ex.Semigroup line 1276 source
instance Ex.Ex.(instance at line 1280) line 1280 source
instance Ex.Ex.(instance at line 1283) line 1283 source
Source comment
----
```
instance : CoeSort Semigroup (Type u) where
…
```
Mentions: Ex.Ex.Semigroup
example Ex.Ex.(example at line 1286) line 1286 source
structure Ex.Ex.Semigroup line 1311 source
instance Ex.Ex.(instance at line 1315) line 1315 source
instance Ex.Ex.(instance at line 1317) line 1317 source
structure Ex.Ex.Morphism line 1320 source
Source comment
----
```
structure Morphism (S1 S2 : Semigroup) where
…
```
Mentions: Ex.Ex.Semigroup
structure Ex.Ex.Semigroup line 1332 source
instance Ex.Ex.(instance at line 1336) line 1336 source
instance Ex.Ex.(instance at line 1338) line 1338 source
structure Ex.Ex.Morphism line 1340 source
instance Ex.Ex.(instance at line 1344) line 1344 source
Source comment
----
```
instance (S1 S2 : Semigroup) :
    CoeFun (Morphism S1 S2) (fun _ => S1 → S2) where
…
```
Mentions: Ex.Ex.Semigroup, Ex.Ex.Morphism
theorem Ex.Ex.resp_mul line 1348 source
example Ex.Ex.(example at line 1352) line 1352 source