Documentation
Lean
.
Meta
.
Tactic
.
Simp
.
BuiltinSimprocs
.
Fin
Search
return to top
source
Imports
Lean.ToExpr
Lean.Meta.LitValues
Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
Imported by
Fin
.
Value
Fin
.
instDecidableEqValue
Fin
.
instReprValue
Fin
.
fromExpr?
Fin
.
reduceOp
Fin
.
reduceNatOp
Fin
.
reduceBin
Fin
.
reduceBinPred
Fin
.
reduceBoolPred
Fin
.
reduceSucc
Fin
.
reduceRev
Fin
.
reduceLast
Fin
.
reduceAdd
Fin
.
reduceMul
Fin
.
reduceSub
Fin
.
reduceDiv
Fin
.
reduceMod
Fin
.
reduceAnd
Fin
.
reduceOr
Fin
.
reduceXor
Fin
.
reduceShiftLeft
Fin
.
reduceShiftRight
Fin
.
reduceLT
Fin
.
reduceLE
Fin
.
reduceGT
Fin
.
reduceGE
Fin
.
reduceEq
Fin
.
reduceNe
Fin
.
reduceBEq
Fin
.
reduceBNe
Fin
.
isValue
Fin
.
reduceFinMk
Fin
.
reduceOfNat
Fin
.
reduceCastSucc
Fin
.
reduceCastAdd
Fin
.
reduceAddNat
Fin
.
reduceNatAdd
Fin
.
reduceCastLT
Fin
.
reduceCastLE
Fin
.
reduceSubNat
Fin
.
reducePred
source
structure
Fin
.
Value
:
Type
n :
Nat
value :
Fin
self
.
n
Instances For
source
instance
Fin
.
instDecidableEqValue
:
DecidableEq
Value
Equations
source
instance
Fin
.
instReprValue
:
Repr
Value
Equations
source
def
Fin
.
fromExpr?
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
(
Option
Value
)
Equations
Instances For
source
@[inline]
def
Fin
.
reduceOp
(
declName
:
Lean.Name
)
(
arity
:
Nat
)
(
f
:
Nat
→
Nat
)
(
op
:
{
n
:
Nat
} →
Fin
n
→
Fin
(
f
n
)
)
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
Lean.Meta.Simp.DStep
Equations
Instances For
source
@[inline]
def
Fin
.
reduceNatOp
(
declName
:
Lean.Name
)
(
arity
:
Nat
)
(
f
:
Nat
→
Nat
)
(
op
:
(
n
:
Nat
) →
Fin
(
f
n
)
)
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
Lean.Meta.Simp.DStep
Equations
Instances For
source
@[inline]
def
Fin
.
reduceBin
(
declName
:
Lean.Name
)
(
arity
:
Nat
)
(
op
:
{
n
:
Nat
} →
Fin
n
→
Fin
n
→
Fin
n
)
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
Lean.Meta.Simp.DStep
Equations
Instances For
source
@[inline]
def
Fin
.
reduceBinPred
(
declName
:
Lean.Name
)
(
arity
:
Nat
)
(
op
:
Nat
→
Nat
→
Bool
)
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
Lean.Meta.Simp.Step
Equations
Instances For
source
@[inline]
def
Fin
.
reduceBoolPred
(
declName
:
Lean.Name
)
(
arity
:
Nat
)
(
op
:
Nat
→
Nat
→
Bool
)
(
e
:
Lean.Expr
)
:
Lean.Meta.SimpM
Lean.Meta.Simp.DStep
Equations
Instances For
source
def
Fin
.
reduceSucc
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceRev
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceLast
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceAdd
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceMul
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceSub
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceDiv
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceMod
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceAnd
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceOr
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceXor
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceShiftLeft
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceShiftRight
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceLT
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceLE
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceGT
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceGE
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceEq
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceNe
:
Lean.Meta.Simp.Simproc
Equations
Instances For
source
def
Fin
.
reduceBEq
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceBNe
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
isValue
:
Lean.Meta.Simp.DSimproc
Simplification procedure for ensuring
Fin
n
literals are normalized.
Equations
Instances For
source
def
Fin
.
reduceFinMk
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceOfNat
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceCastSucc
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceCastAdd
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceAddNat
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceNatAdd
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceCastLT
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceCastLE
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reduceSubNat
:
Lean.Meta.Simp.DSimproc
Equations
Instances For
source
def
Fin
.
reducePred
:
Lean.Meta.Simp.DSimproc
Equations
Instances For