diff --git a/Pantograph/Serial.lean b/Pantograph/Serial.lean index 3d0d945..072872b 100644 --- a/Pantograph/Serial.lean +++ b/Pantograph/Serial.lean @@ -26,6 +26,7 @@ def syntax_from_str (env: Environment) (s: String): Except String Syntax := (fileName := "") +/-- Parse a syntax object. May generate additional metavariables! -/ def syntax_to_expr_type (syn: Syntax): Elab.TermElabM (Except String Expr) := do try let expr ← Elab.Term.elabType syn