## Stream: new members

### Topic: using #reduce and #eval in proofs?

#### Jason Gross (Jul 21 2020 at 19:43):

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 (Jul 21 2020 at 19:48):

#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 (Jul 21 2020 at 19:48):

#reduce is as fast/slow as rfl

#### Kenny Lau (Jul 21 2020 at 19:49):

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

#### Kenny Lau (Jul 21 2020 at 19:49):

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

#### Kenny Lau (Jul 21 2020 at 19:49):

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

#### Jason Gross (Jul 21 2020 at 19:52):

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

Last updated: May 11 2021 at 14:11 UTC