From 9119f47a8f2d1d281975c30a7301a734fbd4eecf Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Sat, 5 Oct 2024 10:29:20 -0700 Subject: [PATCH] chore: Remove more thin wrappers --- Pantograph/Environment.lean | 8 -------- 1 file changed, 8 deletions(-) diff --git a/Pantograph/Environment.lean b/Pantograph/Environment.lean index ef4a40e..040d801 100644 --- a/Pantograph/Environment.lean +++ b/Pantograph/Environment.lean @@ -24,14 +24,6 @@ def module_of_name (env: Environment) (name: Name): Option Name := do let moduleId ← env.getModuleIdxFor? name return env.allImportedModuleNames.get! moduleId.toNat -@[export pantograph_constant_info_is_unsafe_or_partial] -def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial - -@[export pantograph_constant_info_type] -def constantInfoType (info: ConstantInfo): CoreM Expr := unfoldAuxLemmas info.type -@[export pantograph_constant_info_value] -def constantInfoValue (info: ConstantInfo): CoreM (Option Expr) := info.value?.mapM unfoldAuxLemmas - def toCompactSymbolName (n: Name) (info: ConstantInfo): String := let pref := match info with | .axiomInfo _ => "a"