max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(tests/lean/interactive): remove local paths

Browse source
This commit is contained in:
Leonardo de Moura 2016-12-20 12:46:10 -08:00
parent c9e0727ac0
commit a358ea32ac
3 changed files with 5 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
tests/lean/interactive/info1.input
View file

@ -1,2 +1,2 @@
{"seq_num": 0, "command":"sync","file_name":"\/home\/leo\/projects\/lean\/tests\/lean\/interactive\/info1.lean","content":"def foo.f : nat \u2192 nat := \u03bb x, x\ndef bla.f : string \u2192 string := \u03bb x, x\nopen foo bla\nexample : nat :=\nf 0\n"}
{"seq_num": 1, "command":"info","file_name":"\/home\/leo\/projects\/lean\/tests\/lean\/interactive\/info1.lean","line":5,"column":0}
{"seq_num": 0, "command":"sync","file_name":"info1.lean","content":"def foo.f : nat \u2192 nat := \u03bb x, x\ndef bla.f : string \u2192 string := \u03bb x, x\nopen foo bla\nexample : nat :=\nf 0\n"}
{"seq_num": 1, "command":"info","file_name":"info1.lean","line":5,"column":0}

2
tests/lean/interactive/info1.input.expected.out
View file

@ -1,2 +1,2 @@
{"message":"file invalidated","response":"ok","seq_num":0}
{"record":{"full-id":"foo.f","source":{"column":4,"file":"/tests/lean/interactive/info1.lean","line":1},"type":"ℕ → ℕ"},"response":"ok","seq_num":1}
{"record":{"full-id":"foo.f","source":{"column":4,"file":"info1.lean","line":1},"type":"ℕ → ℕ"},"response":"ok","seq_num":1}

4
tests/lean/interactive/info2.input
View file

@ -1,2 +1,2 @@
{"seq_num":0,"command":"sync","file_name":"\/home\/leo\/projects\/lean\/build\/release\/param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\nparameter [decidable_eq nat]\n\nend s1\n"}
{"seq_num":2,"command":"sync","file_name":"\/home\/leo\/projects\/lean\/build\/release\/param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\n\nparameter [decidable_eq nat]\n\nend s1\n"}
{"seq_num":0,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\nparameter [decidable_eq nat]\n\nend s1\n"}
{"seq_num":2,"command":"sync","file_name":"param.lean","content":"section s1\nparameters {\u03b1 \u03b2 : Type}\n\nparameter [decidable_eq \u03b1]\n\nparameter [decidable_eq \u03b2]\nparameter [decidable_eq nat]\n\nparameter [decidable_eq nat]\n\nend s1\n"}