From 16ea00586df7feb863823e59a873dbd0b177038c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 10 Aug 2021 15:06:06 -0700 Subject: [PATCH] fix: fixes #620 --- src/Lean/Meta/Reduce.lean | 7 ++++--- tests/lean/620.lean | 7 +++++++ tests/lean/620.lean.expected.out | 2 ++ 3 files changed, 13 insertions(+), 3 deletions(-) create mode 100644 tests/lean/620.lean create mode 100644 tests/lean/620.lean.expected.out diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean index fbb390dfdf..52fdd8ac2b 100644 --- a/src/Lean/Meta/Reduce.lean +++ b/src/Lean/Meta/Reduce.lean @@ -32,9 +32,10 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta else args ← args.modifyM i visit pure (mkAppN f args) - | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b) - | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b) - | _ => return e + | Expr.lam .. => lambdaTelescope e fun xs b => do mkLambdaFVars xs (← visit b) + | Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b) + | Expr.proj n i s .. => return mkProj n i (← visit s) + | _ => return e visit e |>.run end Lean.Meta diff --git a/tests/lean/620.lean b/tests/lean/620.lean new file mode 100644 index 0000000000..df4a5e6c69 --- /dev/null +++ b/tests/lean/620.lean @@ -0,0 +1,7 @@ +structure Foo (α : Type) where foo : α +class Bar (α β : Type) where coe : α → β + +variable {α : Type} (x : Foo (Foo α)) + +#reduce @Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x -- x.1 +#reduce (@Coe.coe (Foo (Foo α)) (Foo α) (Coe.mk fun y => y.foo) x).1 -- (Coe.coe x).1 instead of x.1.1 diff --git a/tests/lean/620.lean.expected.out b/tests/lean/620.lean.expected.out new file mode 100644 index 0000000000..1d64a03799 --- /dev/null +++ b/tests/lean/620.lean.expected.out @@ -0,0 +1,2 @@ +x.1 +x.1.1