From 20c041b421a7c6d15f78a19cd8f0404bdcd1fc84 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Sep 2020 08:03:52 -0700 Subject: [PATCH] feat: `mkUnsafeRecName` and `isUnsafeRecName?` in Lean --- src/Lean/Compiler/Util.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/src/Lean/Compiler/Util.lean b/src/Lean/Compiler/Util.lean index 1d36a05428..491d3761c4 100644 --- a/src/Lean/Compiler/Util.lean +++ b/src/Lean/Compiler/Util.lean @@ -82,5 +82,19 @@ match env.find? n with | none => Except.error "unknow declaration" | _ => Except.error "declaration is not a definition" +/-- + We generate auxiliary unsafe definitions for regular recursive definitions. + The auxiliary unsafe definition has a clear runtime cost execution model. + This function returns the auxiliary unsafe definition name for the given name. -/ +@[export lean_mk_unsafe_rec_name] +def mkUnsafeRecName (declName : Name) : Name := +mkNameStr declName "_unsafe_rec" + +/-- Return `some _` if the given name was created using `mkUnsafeRecName` -/ +@[export lean_is_unsafe_rec_name] +def isUnsafeRecName? : Name → Option Name +| Name.str n "_unsafe_rec" _ => some n +| _ => none + end Compiler end Lean