backends/lean/Base/Arith/Base.lean


1
2
3
4
5
6
7
8
9
10

import Lean

namespace Arith

open Lean Elab Term Meta

-- We can't define and use trace classes in the same file
initialize registerTraceClass `Arith

end Arith