Documentation
Init.Data.Prod
Google site search
Init.Data.Prod
source
Imports
Init.SimpLemmas
Imported by
Init.Data
Init.Data.Nat.Linear
instLawfulBEqProdInstBEqProd
source
noncomputable instance
instLawfulBEqProdInstBEqProd
{α :
Type u_1
}
{β :
Type u_2
}
[inst :
BEq
α
]
[inst :
BEq
β
]
[inst :
LawfulBEq
α
]
[inst :
LawfulBEq
β
]
:
LawfulBEq
(
α
×
β
)
Equations
@
instLawfulBEqProdInstBEqProd
=
@
instLawfulBEqProdInstBEqProd.proof_1
General documentation
index
Library
Init
Init.Control
Init.Control.Basic
Init.Control.EState
Init.Control.Except
Init.Control.ExceptCps
Init.Control.Id
Init.Control.Lawful
Init.Control.Option
Init.Control.Reader
Init.Control.State
Init.Control.StateCps
Init.Control.StateRef
Init.Data
Init.Data.Array
Init.Data.Array.Basic
Init.Data.Array.BasicAux
Init.Data.Array.BinSearch
Init.Data.Array.DecidableEq
Init.Data.Array.InsertionSort
Init.Data.Array.Mem
Init.Data.Array.QSort
Init.Data.Array.Subarray
Init.Data.ByteArray
Init.Data.ByteArray.Basic
Init.Data.Char
Init.Data.Char.Basic
Init.Data.Fin
Init.Data.Fin.Basic
Init.Data.FloatArray
Init.Data.FloatArray.Basic
Init.Data.Format
Init.Data.Format.Basic
Init.Data.Format.Instances
Init.Data.Format.Macro
Init.Data.Format.Syntax
Init.Data.Int
Init.Data.Int.Basic
Init.Data.List
Init.Data.List.Basic
Init.Data.List.BasicAux
Init.Data.List.Control
Init.Data.Nat
Init.Data.Nat.Basic
Init.Data.Nat.Bitwise
Init.Data.Nat.Control
Init.Data.Nat.Div
Init.Data.Nat.Gcd
Init.Data.Nat.Linear
Init.Data.Nat.Log2
Init.Data.Nat.SOM
Init.Data.Option
Init.Data.Option.Basic
Init.Data.Option.BasicAux
Init.Data.Option.Instances
Init.Data.String
Init.Data.String.Basic
Init.Data.String.Extra
Init.Data.ToString
Init.Data.ToString.Basic
Init.Data.ToString.Macro
Init.Data.AC
Init.Data.Array
Init.Data.Basic
Init.Data.ByteArray
Init.Data.Char
Init.Data.Fin
Init.Data.Float
Init.Data.FloatArray
Init.Data.Format
Init.Data.Hashable
Init.Data.Int
Init.Data.List
Init.Data.Nat
Init.Data.OfScientific
Init.Data.Option
Init.Data.Ord
Init.Data.Prod
Init.Data.Random
Init.Data.Range
Init.Data.Repr
Init.Data.Stream
Init.Data.String
Init.Data.ToString
Init.Data.UInt
Init.System
Init.System.FilePath
Init.System.IO
Init.System.IOError
Init.System.Platform
Init.System.ST
Init.Classical
Init.Coe
Init.Control
Init.Conv
Init.Core
Init.Data
Init.Fix
Init.Hints
Init.Meta
Init.Notation
Init.NotationExtra
Init.Prelude
Init.SimpLemmas
Init.SizeOf
Init.SizeOfLemmas
Init.System
Init.Tactics
Init.Util
Init.WF
Init.WFTactics
Socket
Socket.Basic
Socket.Init
Socket.SockAddr
Socket.Socket