diff options
| author | Son Ho | 2023-12-07 20:52:04 +0100 |
|---|---|---|
| committer | Son Ho | 2023-12-07 20:52:04 +0100 |
| commit | b3ebef29fe3f13a9004b39fcb89afb33fbbfd248 (patch) | |
| tree | a530dfb5c8f45a4a79ce0f03714bb0b90495ee8c /backends/lean/Base/Diverge/ElabBase.lean | |
| parent | f7493580421d31b1d3798521b4f9154e69755f89 (diff) | |
Start working on a version of Diverge.FixI more suited to higher-order functions
Diffstat (limited to '')
| -rw-r--r-- | backends/lean/Base/Diverge/ElabBase.lean | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/backends/lean/Base/Diverge/ElabBase.lean b/backends/lean/Base/Diverge/ElabBase.lean index fedb1c74..1a0676e2 100644 --- a/backends/lean/Base/Diverge/ElabBase.lean +++ b/backends/lean/Base/Diverge/ElabBase.lean @@ -1,8 +1,11 @@ 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 @@ -12,4 +15,7 @@ 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 |