10 lines
187 B
Text
10 lines
187 B
Text
module
|
|
|
|
public def f2 (x : Nat) :=
|
|
x + 1
|
|
|
|
private axiom myAx : f2 x = x + 1
|
|
|
|
@[local cbv_eval] public theorem f2_spec : f2 x = x + 1 := myAx
|
|
|
|
example : f2 1 = 2 := by conv => lhs; cbv
|