Zulip Chat Archive

Stream: general

Topic: norm_num produces bad proof term


Bhavik Mehta (Nov 07 2022 at 19:20):

Here's my example:

import tactic.norm_num

lemma covering_one_aux :  n, n = 6  ¬n % 4 = 0  false :=
begin
  rintro (_ | _ | _ | _ | _ | _ | _ | _) h,
  work_on_goal 7 {norm_num1},
  all_goals {sorry},
end

and it produces the error

type mismatch at application
  norm_num.one_add 2 5 (norm_num.bit0_succ 1)
term
  norm_num.bit0_succ 1
has type
  2 + 1 = 3
but is expected to have type
  2 + 1 = 5

Mario Carneiro (Nov 07 2022 at 20:02):

#17415

Bhavik Mehta (Nov 07 2022 at 22:19):

Thanks!


Last updated: Dec 20 2023 at 11:08 UTC