From 0ae89c16b82fc7bad1fec5233ee374be71adc5bc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 20 Nov 2019 10:45:19 -0800 Subject: [PATCH] chore: move TODO --- library/Init/Lean/Meta.lean | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/library/Init/Lean/Meta.lean b/library/Init/Lean/Meta.lean index de50afa0e3..7e841ed269 100644 --- a/library/Init/Lean/Meta.lean +++ b/library/Init/Lean/Meta.lean @@ -31,15 +31,15 @@ private def boolToExpr : Bool → Expr | true => mkBVar 0 private partial def auxFixpoint : MetaOp → Expr → Expr → MetaM Expr | op, e₁, e₂ => - let whnf := fun e => auxFixpoint whnfOp e e; - let inferType := fun e => auxFixpoint inferTypeOp e e; - let isDefEq := fun e₁ e₂ => pure false; -- TODO - let synthPending := fun e => pure false; -- TODO + let whnf := fun e => auxFixpoint whnfOp e e; + let inferType := fun e => auxFixpoint inferTypeOp e e; + let isDefEq := fun e₁ e₂ => exprToBool <$> auxFixpoint isDefEqOp e₁ e₂; + let synthPending := fun e => exprToBool <$> auxFixpoint synthPendingOp e e; match op with | whnfOp => whnfAux inferType isDefEq synthPending e₁ | inferTypeOp => inferTypeAux whnf e₁ - | synthPendingOp => boolToExpr <$> pure false - | isDefEqOp => boolToExpr <$> pure false + | synthPendingOp => boolToExpr <$> pure false -- TODO + | isDefEqOp => boolToExpr <$> pure false -- TODO def whnf (e : Expr) : MetaM Expr := auxFixpoint whnfOp e e