HepLean Documentation
Mathlib
.
Tactic
.
FunProp
.
Attr
Search
Google site search
return to top
source
Imports
Init
Mathlib.Tactic.FunProp.Decl
Mathlib.Tactic.FunProp.Theorems
Imported by
Mathlib
.
Meta
.
FunProp
.
funPropAttr
funProp
attribute
#
source
opaque
Mathlib
.
Meta
.
FunProp
.
funPropAttr
:
Unit
Initialization of
funProp
attribute