max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: move TODO

Browse source
This commit is contained in:
Leonardo de Moura 2019-11-20 10:45:19 -08:00
parent 771fcdf006
commit 0ae89c16b8
1 changed files with 6 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
library/Init/Lean/Meta.lean
View file

@ -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