Contents
Index
eq-4.2: Leibnizian equality
Index
:=
Data.Eq.Type
:==
Data.Eq.Type.Hetero
coerce
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
fromHomogeneous
Data.Eq.Type.Hetero
fromLeibniz
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
heteroFromLeibniz
Data.Eq.Type.Hetero
heteroToLeibniz
Data.Eq.Type.Hetero
HRefl
Data.Eq.Type.Hetero
hsubst
Data.Eq.Type.Hetero
lift
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lift2
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lift2'
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lift3
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lift3'
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lower
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lower2
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
lower3
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
Refl
Data.Eq.Type
refl
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
reprLeibniz
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
subst
Data.Eq.Type
symm
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
toHomogeneous
Data.Eq.Type.Hetero
toLeibniz
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero
trans
1 (Function)
Data.Eq.Type
2 (Function)
Data.Eq.Type.Hetero