backends/lean/Base/UtilsBase.lean


1
2
3
4
5
6
7
8
9
10

import Lean

namespace Utils

open Lean Elab Term Meta

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

end Utils