Skip to content

Commit 2df8f51

Browse files
authored
chore: shorten pole (#14242)
This PR shortens the pole.
1 parent e281ba8 commit 2df8f51

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

src/Lean/Elab/Tactic/Do/Internal/VCGen/Reduce.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@ module
88
prelude
99
public import Lean.Meta.Sym.SymM
1010
import Lean.Meta.WHNF
11-
import Lean.Meta.Sym
11+
import Lean.Meta.Sym.Util
1212

1313
open Lean Meta Sym
1414

0 commit comments

Comments
 (0)