doc: TermElabM metavariable generation

This commit is contained in:
Leni Aniva 2023-12-08 17:32:30 -08:00
parent bd0c66facc
commit ac9f6f810c
1 changed files with 1 additions and 0 deletions

View File

@ -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