Documentation
Qq
.
AssertInstancesCommute
Search
Google site search
Qq
.
AssertInstancesCommute
source
Imports
Init
Qq.MetaM
Imported by
Qq
.
termAssumeInstancesCommute'_
Qq
.
Impl
.
isRedundantLocalInst?
Qq
.
Impl
.
findRedundantLocalInst?
Qq
.
Impl
.
findRedundantLocalInstQuoted?
Qq
.
Impl
.
termAssertInstancesCommuteImpl_
Qq
.
Impl
.
termAssertInstancesCommuteDummy
Qq
.
Impl
.
termAssumeInstancesCommuteDummy
Qq
.
doElemAssertInstancesCommute
Qq
.
doElemAssumeInstancesCommute
source
def
Qq
.
termAssumeInstancesCommute'_
:
Lean.ParserDescr
Instances For
source
def
Qq
.
Impl
.
isRedundantLocalInst?
(inst :
Lean.FVarId
)
:
Lean.MetaM
(
Option
Lean.Expr
)
Instances For
source
def
Qq
.
Impl
.
findRedundantLocalInst?
:
Qq.Impl.QuoteM
(
Option
(
Lean.FVarId
×
Lean.Expr
)
)
Instances For
source
def
Qq
.
Impl
.
findRedundantLocalInstQuoted?
:
Lean.Elab.TermElabM
(
Option
(
Lean.FVarId
×
(u :
Q(
Lean.Level
)
) ×
(ty :
Q(
Q(
Sort
«$u»)
)
) ×
Q(
Q(
«$$ty»
)
)
×
Q(
Q(
«$$ty»
)
)
)
)
Instances For
source
def
Qq
.
Impl
.
termAssertInstancesCommuteImpl_
:
Lean.ParserDescr
Instances For
source
def
Qq
.
Impl
.
termAssertInstancesCommuteDummy
:
Lean.ParserDescr
Instances For
source
def
Qq
.
Impl
.
termAssumeInstancesCommuteDummy
:
Lean.ParserDescr
Instances For
source
def
Qq
.
doElemAssertInstancesCommute
:
Lean.ParserDescr
Instances For
source
def
Qq
.
doElemAssumeInstancesCommute
:
Lean.ParserDescr
Instances For