aniva/Pantograph
aniva
/
Pantograph
1
1
Fork 0
Code Issues 10 Pull Requests 1 Packages Projects Releases 1 Wiki Activity

feat: Add support for the have, conv, and calc tactics #59

Merged
aniva merged 22 commits from goal/have-conv-calc into dev 2024-04-11 15:36:20 -07:00
Conversation 0 Commits 22 Files Changed 9 +6 -8
1 changed files with 6 additions and 8 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files
Showing only changes of commit ea0f411949 - Show all commits

14
Pantograph/Serial.lean
View File

@ -160,14 +160,12 @@ partial def serialize_expression_ast (expr: Expr) (sanitize: Bool := true): Meta
of_name (name: Name) := name_to_ast name sanitize of_name (name: Name) := name_to_ast name sanitize
def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do def serialize_expression (options: @&Protocol.Options) (e: Expr): MetaM Protocol.Expression := do
let pp := toString (← Meta.ppExpr e) let pp?: Option String ← match options.printExprPretty with
let pp?: Option String := match options.printExprPretty with | true => pure $ .some $ toString $ ← Meta.ppExpr e
| true => .some pp | false => pure $ .none
| false => .none let sexp?: Option String ← match options.printExprAST with
let sexp: String ← serialize_expression_ast e | true => pure $ .some $ ← serialize_expression_ast e
let sexp?: Option String := match options.printExprAST with | false => pure $ .none
| true => .some sexp
| false => .none
return { return {
pp?, pp?,
sexp? sexp?