fix: Leading element in .proj sexp
This commit is contained in:
parent
9cc770c3c9
commit
56cfe523df
|
@ -155,7 +155,7 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
|
|||
|
||||
let autos := String.intercalate " " (List.replicate ctor.numParams "_")
|
||||
let inner ← self inner
|
||||
pure s!"(:app (:c {projectorName}) {autos} {inner})"
|
||||
pure s!"((:c {projectorName}) {autos} {inner})"
|
||||
-- Elides all unhygenic names
|
||||
binder_info_to_ast : Lean.BinderInfo → String
|
||||
| .default => ""
|
||||
|
|
|
@ -74,7 +74,7 @@ def test_sexp_of_expr (env: Environment): IO LSpec.TestSeq := do
|
|||
.default)
|
||||
.implicit)
|
||||
.implicit,
|
||||
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) (:app (:c And.right) _ _ 0)) :implicit) :implicit)"
|
||||
"(:lambda p (:sort 0) (:lambda q (:sort 0) (:lambda k ((:c And) 1 0) ((:c And.right) _ _ 0)) :implicit) :implicit)"
|
||||
),
|
||||
]
|
||||
let termElabM: Elab.TermElabM LSpec.TestSeq := entries.foldlM (λ suites (expr, target) => do
|
||||
|
|
Loading…
Reference in New Issue