From d138d068dd2ecedc4628e5483f71ba4b36b148fa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 11 Nov 2019 08:41:17 -0800 Subject: [PATCH] chore: fix typo --- library/Init/Lean/Meta/Default.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/Init/Lean/Meta/Default.lean b/library/Init/Lean/Meta/Default.lean index 9707322ea2..57b0b6c9ad 100644 --- a/library/Init/Lean/Meta/Default.lean +++ b/library/Init/Lean/Meta/Default.lean @@ -37,9 +37,9 @@ private partial def auxFixpoint : MetaOp → Expr → Expr → MetaM Expr let synthPending := fun e => pure false; -- TODO match op with | whnfOp => whnfAux inferType isDefEq synthPending e₁ - | inferTypeOp => inferType e₁ - | synthPendingOp => boolToExpr <$> synthPending e₁ - | isDefEqOp => boolToExpr <$> isDefEq e₁ e₂ + | inferTypeOp => inferTypeAux whnf e₁ + | synthPendingOp => boolToExpr <$> pure false + | isDefEqOp => boolToExpr <$> pure false def whnf (e : Expr) : MetaM Expr := auxFixpoint whnfOp e e