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

chore: Code formatting

This commit is contained in:
Leni Aniva 2023-11-06 12:20:08 -08:00
parent 245e76b2f1
commit 7076669c3d
Signed by: aniva
GPG Key ID: 4D9B1C8D10EA4C50
1 changed files with 11 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
Pantograph.lean
View File

@ -29,17 +29,17 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
| .error ierror => return Lean.toJson ierror
| .error error => return Lean.toJson $ errorCommand s!"Unable to parse json: {error}"
match command.cmd with
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog
| "lib.inspect" => run lib_inspect
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete
| "reset" => run reset
| "stat" => run stat
| "expr.echo" => run expr_echo
| "lib.catalog" => run lib_catalog
| "lib.inspect" => run lib_inspect
| "options.set" => run options_set
| "options.print" => run options_print
| "goal.start" => run goal_start
| "goal.tactic" => run goal_tactic
| "goal.continue" => run goal_continue
| "goal.delete" => run goal_delete
| "goal.print" => run goal_print
| cmd =>
let error: Protocol.InteractionError :=