test: and fix
diff --git a/src/Lean/Meta/Sym/LooseBVarsS.lean b/src/Lean/Meta/Sym/LooseBVarsS.lean index ae5b251..87f725f 100644 --- a/src/Lean/Meta/Sym/LooseBVarsS.lean +++ b/src/Lean/Meta/Sym/LooseBVarsS.lean
@@ -7,6 +7,7 @@ prelude public import Lean.Meta.Sym.SymM import Lean.Meta.Sym.ReplaceS +public section namespace Lean.Meta.Sym /--
diff --git a/src/Lean/Meta/Sym/ReplaceS.lean b/src/Lean/Meta/Sym/ReplaceS.lean index 83473aa..6d8278a 100644 --- a/src/Lean/Meta/Sym/ReplaceS.lean +++ b/src/Lean/Meta/Sym/ReplaceS.lean
@@ -35,8 +35,8 @@ | .app f a => mkAppS (← visitChild f offset fn) (← visitChild a offset fn) | .mdata m a => mkMDataS m (← visitChild a offset fn) | .proj s i a => mkProjS s i (← visitChild a offset fn) - | .forallE n d b bi => mkForallS n bi (← visitChild d offset fn) (← visitChild d (offset+1) fn) - | .lam n d b bi => mkLambdaS n bi (← visitChild d offset fn) (← visitChild d (offset+1) fn) + | .forallE n d b bi => mkForallS n bi (← visitChild d offset fn) (← visitChild b (offset+1) fn) + | .lam n d b bi => mkLambdaS n bi (← visitChild d offset fn) (← visitChild b (offset+1) fn) | .letE n t v b d => mkLetS n (← visitChild t offset fn) (← visitChild v offset fn) (← visitChild b (offset+1) fn) (nondep := d) end
diff --git a/tests/lean/run/sym_liftLower.lean b/tests/lean/run/sym_liftLower.lean new file mode 100644 index 0000000..c12ff22 --- /dev/null +++ b/tests/lean/run/sym_liftLower.lean
@@ -0,0 +1,23 @@ +import Lean.Meta.Sym + +open Lean Meta Grind Sym + +def tst1 : SymM Unit := do + let x1 ← mkBVarS 0 + let x2 ← mkBVarS 1 + let t1 ← mkAppS (← mkAppS (← mkConstS `f) x1) x2 + let t2 ← mkForallS `x BinderInfo.default (← mkConstS `Nat) t1 + IO.println (← liftLooseBVarsS t1 0 1) + IO.println (← liftLooseBVarsS t2 0 1) + let t3 ← lowerLooseBVarsS (← liftLooseBVarsS t2 0 1) 1 1 + IO.println t3 + assert! t2 == t3 + assert! isSameExpr t2 t3 + +/-- +info: f #1 #2 +forall (x : Nat), f x #1 +forall (x : Nat), f x #0 +-/ +#guard_msgs in +#eval SymM.run' tst1