5 lines
86 B
Plaintext
5 lines
86 B
Plaintext
|
import Mathlib.Tactic
|
||
|
|
import Mathlib.Util.PiNotation
|
||
|
|
|
||
|
|
set_option warningAsError false
|