Simplify test

Author: augustepoiroux

test/set_option.expected.out

@@ -1,21 +1,21 @@
 {"messages":
  [{"severity": "info",
-   "pos": {"line": 8, "column": 0},
-   "endPos": {"line": 8, "column": 8},
-   "data": "Elab.async = false"}],
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 6},
+   "data": "1 : Nat"}],
  "env": 0}
 
 {"messages":
  [{"severity": "info",
-   "pos": {"line": 10, "column": 0},
-   "endPos": {"line": 10, "column": 8},
-   "data": "Elab.async = true"}],
+   "pos": {"line": 2, "column": 0},
+   "endPos": {"line": 2, "column": 6},
+   "data": "(1 : Nat) : Nat"}],
  "env": 1}
 
 {"messages":
  [{"severity": "info",
-   "pos": {"line": 8, "column": 0},
-   "endPos": {"line": 8, "column": 8},
-   "data": "Elab.async = true"}],
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 6},
+   "data": "(1 : Nat) : Nat"}],
  "env": 2}
 

test/set_option.in

@@ -1,6 +1,6 @@
-{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"}
+{"cmd": "#check 1"}
 
-{"cmd": "import Lean\nopen Lean Elab Command\n\nset_option Elab.async true\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp"}
+{"cmd": "set_option pp.numericTypes true\n#check 1"}
 
-{"cmd": "import Lean\nopen Lean Elab Command\n\nelab \"#show_pp\" : command => do\n  let o ← getOptions\n  logInfo m!\"Elab.async = {Elab.async.get o}\"\n\n#show_pp", "setOptions":[[["Elab","async"],true]]}
+{"cmd": "#check 1", "setOptions":[[["pp","numericTypes"],true]]}