fix: Printing projection leads to crash

This commit is contained in:
Leni Aniva 2023-12-05 22:45:59 -08:00
parent 56966b27cf
commit ccf5a03647
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
3 changed files with 7 additions and 6 deletions

View File

@ -119,7 +119,7 @@ structure LibInspect where
structure LibInspectResult where structure LibInspectResult where
type: Expression type: Expression
value?: Option Expression := .none value?: Option Expression := .none
module?: Option String module?: Option String := .none
-- If the name is private, displays the public facing name -- If the name is private, displays the public facing name
publicName?: Option String := .none publicName?: Option String := .none
typeDependency?: Option (Array String) := .none typeDependency?: Option (Array String) := .none

View File

@ -145,9 +145,9 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
| .proj typeName idx inner => do | .proj typeName idx inner => do
let env ← getEnv let env ← getEnv
let fieldName := getStructureFields env typeName |>.get! idx let fieldName := getStructureFields env typeName |>.get! idx
let inner ← Meta.mkProjection inner fieldName let projectorName := getProjFnForField? env typeName fieldName |>.get!
assert! !inner.isProj let e := Expr.app (.const projectorName []) inner
self inner self e
-- Elides all unhygenic names -- Elides all unhygenic names
binder_info_to_ast : Lean.BinderInfo → String binder_info_to_ast : Lean.BinderInfo → String
| .default => "" | .default => ""

View File

@ -1,4 +1,4 @@
{"version": 5, {"version": 6,
"packagesDir": "lake-packages", "packagesDir": "lake-packages",
"packages": "packages":
[{"git": [{"git":
@ -8,4 +8,5 @@
"opts": {}, "opts": {},
"name": "LSpec", "name": "LSpec",
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41", "inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
"inherited": false}}]} "inherited": false}}],
"name": "pantograph"}