From 97057e56e0ef2b34887844e4517a2180d1073f90 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 10 Feb 2020 19:06:34 -0800 Subject: [PATCH] feat: add `isTypeFormer` --- src/Init/Lean/Meta/InferType.lean | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean index a52932ec4d..00d1147c4a 100644 --- a/src/Init/Lean/Meta/InferType.lean +++ b/src/Init/Lean/Meta/InferType.lean @@ -327,5 +327,22 @@ match r with | Expr.sort _ _ => pure true | _ => pure false +partial def isTypeFormerAux : Expr → MetaM Bool +| type => do + type ← whnfD type; + match type with + | Expr.sort _ _ => pure true + | Expr.forallE n d b c => + withLocalDecl n d c.binderInfo $ fun fvar => + isTypeFormerAux (b.instantiate1 fvar) + | _ => pure false + +/-- + Return true iff `e : Sort _` or `e : (forall As, Sort _)`. + Remark: it subsumes `isType` -/ +def isTypeFormer (e : Expr) : MetaM Bool := do +type ← inferType e; +isTypeFormerAux type + end Meta end Lean