Zulip Chat Archive

Stream: general

Topic: norm_num bug


view this post on Zulip Calle Sönne (Nov 08 2018 at 19:11):

Here is what I think is a bug in norm_num:

import tactic.norm_num
import analysis.real

example : ((8 : ) : ) < 9 := by norm_num

"tactic failed"

view this post on Zulip Simon Hudon (Nov 09 2018 at 18:25):

@Mario Carneiro is norm_num supposed to handle coercions?

view this post on Zulip Mario Carneiro (Nov 09 2018 at 19:13):

no, or at least it has not been extended to coercions

view this post on Zulip Simon Hudon (Nov 10 2018 at 21:16):

That could be a nice feature

view this post on Zulip Kevin Buzzard (Nov 10 2018 at 21:29):

In the mean time, following the tips at https://github.com/leanprover/mathlib/blob/master/docs/extras/casts.md, you can always do this:

import tactic.norm_num
import analysis.real

example : ((8 : ) : ) < 9 := begin
  rw (show ((8 : ) : ) = (8 : ), by simp),
  norm_num
end

view this post on Zulip Nicholas Scheel (Nov 11 2018 at 12:14):

I once made a stupid tactic to do exactly this: https://github.com/MonoidMusician/MATH361/blob/lean-3.4.1/src/naturally.lean

view this post on Zulip Nicholas Scheel (Nov 11 2018 at 12:17):

you can also do the same with rat


Last updated: May 12 2021 at 23:13 UTC