Documentation
Semantic
.
Prelude
Search
return to top
source
Imports
Init
Imported by
HasDenotation
«term⟦_⟧_[_]»
HasExpDenotation
«term⟦_⟧e_[_]»
source
class
HasDenotation
(
T
Env
:
Type
)
(
Denot
:
outParam
Type
)
:
Type
interp :
Env
→
T
→
Denot
Instances
source
def
«term⟦_⟧_[_]»
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For
source
class
HasExpDenotation
(
T
Env
:
Type
)
(
Denot
:
outParam
Type
)
:
Type
interp :
Env
→
T
→
Denot
Instances
source
def
«term⟦_⟧e_[_]»
:
Lean.ParserDescr
Equations
One or more equations did not get rendered due to their size.
Instances For