computational reflection in 3 lines

Stream: general

[Mario Carneiro]

I managed to write a mini norm_num using computational reflection in only a few basic tactics:

import data.num.lemmas
example : 12402536340 * 2356324602 = 29224401505141036680 :=
begin
  rw ← num.of_nat_inj,
  simp [num.bit0_of_bit0, num.bit1_of_bit1],
  refl
end

[Mario Carneiro]

(The original theorem is on nat, so a straight rfl proof times out)

[Kevin Buzzard]

That is very cool :-)

[Johan Commelin]

Cool! Now we can start porting Sage to Lean!

[Johan Commelin]

Do some serious algebraic number theory.