From 2d65b2ba9fa9dfd84de383327f47ae98132f13a2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 1 Nov 2019 17:07:38 -0700 Subject: [PATCH] feat: reduce `Expr.proj` --- library/Init/Lean/TypeUtil.lean | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/library/Init/Lean/TypeUtil.lean b/library/Init/Lean/TypeUtil.lean index 50d8965bf3..8e4d9c99fd 100644 --- a/library/Init/Lean/TypeUtil.lean +++ b/library/Init/Lean/TypeUtil.lean @@ -174,11 +174,13 @@ export AbstractMetavarContext (hasAssignableLevelMVar isReadOnlyLevelMVar auxMVa | _ => -- TODO: auxiliary recursors done () - | e@(Expr.proj _ i m) => do - m ← whnf m; - let f := m.getAppFn; - -- TODO check if `f` is constructor and reduce - pure e + | e@(Expr.proj _ i c) => do + c ← whnf c; + env ← getEnv; + matchConst env c.getAppFn (fun _ => pure e) $ fun cinfo lvls => + match cinfo with + | ConstantInfo.ctorInfo ctorVal => pure $ c.getArgD (ctorVal.nparams + i) e + | _ => pure e | _ => unreachable! /- ===========================