chore: remove dead code
This commit is contained in:
parent
f9b79092f6
commit
868a43a747
1 changed files with 0 additions and 5 deletions
|
|
@ -71,9 +71,4 @@ def TerminationHint.ensureIsEmpty (t : TerminationHint) : MacroM Unit := do
|
|||
| TerminationHint.many m => m.forM fun _ v => Macro.throwErrorAt v.ref "unused termination hint element"
|
||||
| _ => pure ()
|
||||
|
||||
structure TerminationStrategy where
|
||||
terminationBy : TerminationHint := TerminationHint.none
|
||||
decreasingTactic : TerminationHint := TerminationHint.none
|
||||
deriving Inhabited
|
||||
|
||||
end Lean.Elab.WF
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue