ElabBase.lean « Diverge « Base « lean « backends - aeneas - aeneas rust verifier with a hacky Isabelle backend

summary refs log tree commit diff

path: root/backends/lean/Base/Diverge/ElabBase.lean

blob: e693dce28d9d1e41283f3b28b7481d1025744e65 (plain)

import Lean

namespace Diverge

open Lean

initialize registerTraceClass `Diverge.divRecursion (inherited := true)

end Diverge