panic while testing ring tactic

Stream: lean4

[Scott Morrison]

I was thinking about benchmarking the new ring tactic, available now in mathlib4, but encountered a panic:

import Mathlib.Tactic.Ring

-- Causes `PANIC at Lean.Expr.getRevArg! Lean.Expr:508:22: invalid index`:
example (A B C D E F G H I J : ℕ) : ((((((1 : ℕ) ^ 2) + (((((((J ^ 1) + F) * (1 : ℕ)) ^ 0) * (1 : ℕ)) * (((B ^ 1) ^ 0) * (D + (C + (0 : ℕ))))) * ((J * ((1 : ℕ) + (((1 : ℕ) + ((2 : ℕ) + ((I * (H ^ 1)) * (1 : ℕ)))) ^ 0))) ^ 1))) + (((A * (((1 : ℕ) ^ 1) ^ 0)) + ((A + (((1 : ℕ) ^ 1) + (1 : ℕ))) ^ 0)) + (((1 : ℕ) ^ 1) + D))) ^ 2) ^ 2) = ((((((1 : ℕ) ^ 2) + (((((((J ^ 1) + F) * (1 : ℕ)) ^ 0) * (1 : ℕ)) * (((B ^ 1) ^ 0) * (D + (C + (0 : ℕ))))) * ((J * ((1 : ℕ) + (((1 : ℕ) + ((2 : ℕ) + ((I * (H ^ 1)) * (1 : ℕ)))) ^ 0))) ^ 1))) + (((A * (((1 : ℕ) ^ 1) ^ 0)) + ((A + (((1 : ℕ) ^ 1) + (1 : ℕ))) ^ 0)) + (((1 : ℕ) ^ 1) + D))) ^ 2) ^ 2) := by ring

[Notification Bot]

This topic was moved by Scott Morrison to #mathlib4 > panic while testing ring tactic