7d32030729
This PR adds `cbv_eval` attribute that allows to evaluate functions in `cbv` tactic using pre-registered theorems.
7 lines
89 B
Text
7 lines
89 B
Text
module
|
|
|
|
public def f3 (x : Nat) :=
|
|
x + 1
|
|
|
|
@[expose] public def f4 (x : Nat) :=
|
|
x + 1
|