using #reduce and #eval in proofs?

Stream: new members

[Jason Gross]

Is there a way to use the output of #reduce and/or #eval in defining a constant without copy/paste? def foo : ℕ := #reduce (0 + 1) gives error: invalid expression, unexpected token and warning: declaration 'foo' uses sorry

[Kenny Lau]

#eval is unsafe and/so it is faster and/so you basically can't use it (usually norm_num works in this situation)

[Kenny Lau]

#reduce is as fast/slow as rfl

[Kenny Lau]

note that 0 + 1 already defines a natural number, so you don't need to reduce it

[Kenny Lau]

how you could use it would be theorem foo : 0 + 1 = [copy result of #reduce] := rfl

[Kenny Lau]

and theorem foo : 0 + 1 = [copy result of #eval] := by norm_num

[Jason Gross]

norm_num has asymptotically quadratic performance in the size of the term I'm building (even though my algorithm is obviously linear) and so seems to be unsuitable (maybe I'm using it wrong). I want a replacement for something like theorem foo : Σ v, v = 0 + 1 := by { eapply sigma.mk, norm_num } which is faster