blob: fedb1c74a6721f72a1201941a80ac35e0b944021 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
import Lean
namespace Diverge
open Lean Elab Term Meta
-- We can't define and use trace classes in the same file
initialize registerTraceClass `Diverge.elab
initialize registerTraceClass `Diverge.def
initialize registerTraceClass `Diverge.def.sigmas
initialize registerTraceClass `Diverge.def.genBody
initialize registerTraceClass `Diverge.def.valid
initialize registerTraceClass `Diverge.def.unfold
end Diverge
|
