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

feat: Export constant info type/value

This commit is contained in:
Leni Aniva 2024-07-29 18:39:22 -07:00
parent 7b5567d784
commit 1c9a411d4d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 8 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
Pantograph/Environment.lean
View File

@ -16,10 +16,10 @@ def isNameInternal (n: Name): Bool :=
| .str _ name => name == "Lean" | .str _ name => name == "Lean"
| _ => true | _ => true
/-- Catalog all the non-internal names -/ /-- Catalog all the non-internal and safe names -/
@[export pantograph_environment_catalog] @[export pantograph_environment_catalog]
def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name _ => def env_catalog (env: Environment): Array Name := env.constants.fold (init := #[]) (λ acc name info =>
match isNameInternal name with match isNameInternal name || info.isUnsafe with
| false => acc.push name | false => acc.push name
| true => acc) | true => acc)
@ -31,6 +31,11 @@ def module_of_name (env: Environment) (name: Name): Option Name := do
@[export pantograph_constant_info_is_unsafe_or_partial] @[export pantograph_constant_info_is_unsafe_or_partial]
def constantInfoIsUnsafeOrPartial (info: ConstantInfo): Bool := info.isUnsafe || info.isPartial 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"