From 56cfe523df16427a0a2d3b1b4c84630ff2d69be0 Mon Sep 17 00:00:00 2001 From: Leni Aniva Date: Tue, 9 Apr 2024 10:06:26 -0700 Subject: [PATCH] fix: Leading element in .proj sexp --- Pantograph/Serial.lean | 2 +- Test/Serial.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 66abf63..17629ab 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -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 => "" diff --git a/Test/Serial.lean b/Test/Serial.lean index 0dac925..e9f4d85 100644 --- a/Test/Serial.lean +++ b/Test/Serial.lean @@ -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