From 868a43a7471418e71d3a76cb5ee1aebe98f26622 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 11 Jan 2022 16:22:20 -0800 Subject: [PATCH] chore: remove dead code --- src/Lean/Elab/PreDefinition/WF/TerminationHint.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean index e4e265ae80..4872df47f4 100644 --- a/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean +++ b/src/Lean/Elab/PreDefinition/WF/TerminationHint.lean @@ -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