aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

chore: Remove more thin wrappers

This commit is contained in:
Leni Aniva 2024-10-05 10:29:20 -07:00
parent 3c808506c1
commit b9b8265fd5
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 0 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
Pantograph/Environment.lean
View File

@ -24,14 +24,6 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
let moduleId ← env.getModuleIdxFor? name let moduleId ← env.getModuleIdxFor? name
return env.allImportedModuleNames.get! moduleId.toNat 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 := def toCompactSymbolName (n: Name) (info: ConstantInfo): String :=
let pref := match info with let pref := match info with
| .axiomInfo _ => "a" | .axiomInfo _ => "a"