fix: Printing projection leads to crash
This commit is contained in:
parent
f2b54ec018
commit
8a8db545a5
|
@ -119,7 +119,7 @@ structure LibInspect where
|
|||
structure LibInspectResult where
|
||||
type: Expression
|
||||
value?: Option Expression := .none
|
||||
module?: Option String
|
||||
module?: Option String := .none
|
||||
-- If the name is private, displays the public facing name
|
||||
publicName?: Option String := .none
|
||||
typeDependency?: Option (Array String) := .none
|
||||
|
|
|
@ -145,9 +145,9 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
|||
| .proj typeName idx inner => do
|
||||
let env ← getEnv
|
||||
let fieldName := getStructureFields env typeName |>.get! idx
|
||||
let inner ← Meta.mkProjection inner fieldName
|
||||
assert! !inner.isProj
|
||||
self inner
|
||||
let projectorName := getProjFnForField? env typeName fieldName |>.get!
|
||||
let e := Expr.app (.const projectorName []) inner
|
||||
self e
|
||||
-- Elides all unhygenic names
|
||||
binder_info_to_ast : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
|
|
|
@ -1,4 +1,4 @@
|
|||
{"version": 5,
|
||||
{"version": 6,
|
||||
"packagesDir": "lake-packages",
|
||||
"packages":
|
||||
[{"git":
|
||||
|
@ -8,4 +8,5 @@
|
|||
"opts": {},
|
||||
"name": "LSpec",
|
||||
"inputRev?": "88f7d23e56a061d32c7173cea5befa4b2c248b41",
|
||||
"inherited": false}}]}
|
||||
"inherited": false}}],
|
||||
"name": "pantograph"}
|
||||
|
|
Loading…
Reference in New Issue