Lean4
/-- Command that printins all function properties attached to a function.
For example
```
#print_fun_prop_theorems HAdd.hAdd
```
might print out
```
Continuous
continuous_add, args: [4,5], priority: 1000
continuous_add_left, args: [5], priority: 1000
continuous_add_right, args [4], priority: 1000
...
Differentiable
Differentiable.add, args: [4,5], priority: 1000
Differentiable.add_const, args: [4], priority: 1000
Differentiable.const_add, args: [5], priority: 1000
...
```
You can also see only theorems about a concrete function property
```
#print_fun_prop_theorems HAdd.hAdd Continuous
```
-/
@[command_parser 1000]
public meta def «command#print_fun_prop_theorems__» : Lean.ParserDescr✝ :=
ParserDescr.node✝ `Mathlib.Meta.FunProp.«command#print_fun_prop_theorems__» 1022
(ParserDescr.binary✝ `andthen
(ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ "#print_fun_prop_theorems ") (ParserDescr.const✝ `ident))
(ParserDescr.unary✝ `optional (ParserDescr.const✝ `ident)))
