Documentation
Lean
.
Compiler
.
CSimpAttr
Search
return to top
source
Imports
Lean.ScopedEnvExtension
Lean.Util.Recognizers
Lean.Util.ReplaceExpr
Imported by
Lean
.
Compiler
.
CSimp
.
Entry
Lean
.
Compiler
.
CSimp
.
instInhabitedEntry
Lean
.
Compiler
.
CSimp
.
State
Lean
.
Compiler
.
CSimp
.
instInhabitedState
Lean
.
Compiler
.
CSimp
.
State
.
switch
Lean
.
Compiler
.
CSimp
.
ext
Lean
.
Compiler
.
CSimp
.
add
Lean
.
Compiler
.
CSimp
.
replaceConstants
Lean
.
Compiler
.
hasCSimpAttribute
source
structure
Lean
.
Compiler
.
CSimp
.
Entry
:
Type
fromDeclName :
Name
toDeclName :
Name
thmName :
Name
Instances For
source
instance
Lean
.
Compiler
.
CSimp
.
instInhabitedEntry
:
Inhabited
Entry
Equations
source
structure
Lean
.
Compiler
.
CSimp
.
State
:
Type
map :
SMap
Name
Name
thmNames :
SSet
Name
Instances For
source
instance
Lean
.
Compiler
.
CSimp
.
instInhabitedState
:
Inhabited
State
Equations
source
def
Lean
.
Compiler
.
CSimp
.
State
.
switch
:
State
→
State
Equations
Instances For
source
opaque
Lean
.
Compiler
.
CSimp
.
ext
:
SimpleScopedEnvExtension
Entry
State
source
def
Lean
.
Compiler
.
CSimp
.
add
(
declName
:
Name
)
(
kind
:
AttributeKind
)
:
CoreM
Unit
Equations
Instances For
source
@[export lean_csimp_replace_constants]
def
Lean
.
Compiler
.
CSimp
.
replaceConstants
(
env
:
Environment
)
(
e
:
Expr
)
:
Expr
Equations
Instances For
source
def
Lean
.
Compiler
.
hasCSimpAttribute
(
env
:
Environment
)
(
declName
:
Name
)
:
Bool
Equations
Instances For