blob: 1a0676e205775106f9bd30dfb79115cdd9f99bd2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
import Lean
import Base.Utils
import Base.Primitives.Base
namespace Diverge
open Lean Elab Term Meta
open Utils
-- 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
-- For the attribute (for higher-order functions)
initialize registerTraceClass `Diverge.attr
end Diverge
|
