From 45beca0bc4b9b6df45a945c9ab2504fb6332967a Mon Sep 17 00:00:00 2001
From: Leni Aniva <v@leni.sh>
Date: Fri, 8 Dec 2023 17:32:30 -0800
Subject: [PATCH] doc: TermElabM metavariable generation

---
 Pantograph/Serial.lean | 1 +
 1 file changed, 1 insertion(+)

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 := "<stdin>")
 
 
+/-- 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