From 29cb4e993b40739e827714864296fbaa03cd6418 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Oct 2020 15:27:33 -0700 Subject: [PATCH] chore: export `lean_is_io_unit_regular_init_fn` and `lean_is_io_unit_builtin_init_fn` --- src/Lean/Compiler/InitAttr.lean | 24 ++++++++++++++++-------- 1 file changed, 16 insertions(+), 8 deletions(-) diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 460b23abaa..b7a3d8b168 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/src/Lean/Compiler/InitAttr.lean @@ -57,18 +57,26 @@ getInitFnNameForCore? env builtinInitAttr fn def getRegularInitFnNameFor? (env : Environment) (fn : Name) : Option Name := getInitFnNameForCore? env regularInitAttr fn --- Only used -def isIOUnitInitFn (env : Environment) (fn : Name) : Bool := -let aux (attr : ParametricAttribute Name) : Bool := - match attr.getParam env fn with - | some Name.anonymous => true - | _ => false -aux builtinInitAttr || aux regularInitAttr - @[export lean_get_init_fn_name_for] def getInitFnNameFor? (env : Environment) (fn : Name) : Option Name := getBuiltinInitFnNameFor? env fn <|> getRegularInitFnNameFor? env fn +def isIOUnitInitFnCore (env : Environment) (attr : ParametricAttribute Name) (fn : Name) : Bool := +match attr.getParam env fn with +| some Name.anonymous => true +| _ => false + +@[export lean_is_io_unit_regular_init_fn] +def isIOUnitRegularInitFn (env : Environment) (fn : Name) : Bool := +isIOUnitInitFnCore env regularInitAttr fn + +@[export lean_is_io_unit_builtin_init_fn] +def isIOUnitBuiltinInitFn (env : Environment) (fn : Name) : Bool := +isIOUnitInitFnCore env builtinInitAttr fn + +def isIOUnitInitFn (env : Environment) (fn : Name) : Bool := +isIOUnitBuiltinInitFn env fn || isIOUnitRegularInitFn env fn + def hasInitAttr (env : Environment) (fn : Name) : Bool := (getInitFnNameFor? env fn).isSome