Skip to content

Commit

Permalink
copy *.leanInk over *.leanInk.expected
Browse files Browse the repository at this point in the history
  • Loading branch information
@semorrison
semorrison committed Aug 23, 2023
1 parent 39aa884 commit 616aca4
Show file tree
Hide file tree
Showing 19 changed files with 5,193 additions and 44,249 deletions.
38,918 changes: 4,388 additions & 34,530 deletions test/bench/Basic.lean.leanInk.expected
View file

Large diffs are not rendered by default.

96 changes: 6 additions & 90 deletions test/bugs/GH_15.lean.leanInk.expected
View file
Original file line number Diff line number Diff line change
@@ -1,75 +1,7 @@
[{"contents":
[{"typeinfo": {"type": "Nat → Nat", "name": "example", "_type": "typeinfo"},
"semanticType": "Keyword",
"raw": "example",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": " : ",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": {"type": "Type", "name": "Nat", "_type": "typeinfo"},
"semanticType": null,
"raw": "Nat",
"link": null,
"docstring":
"The type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n",
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": " → ",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": {"type": "Type", "name": "Nat", "_type": "typeinfo"},
"semanticType": null,
"raw": "Nat",
"link": null,
"docstring":
"The type of natural numbers, starting at zero. It is defined as an\ninductive type freely generated by \"zero is a natural number\" and\n\"the successor of a natural number is a natural number\".\n\nYou can prove a theorem `P n` about `n : Nat` by `induction n`, which will\nexpect a proof of the theorem for `P 0`, and a proof of `P (succ i)` assuming\na proof of `P i`. The same method also works to define functions by recursion\non natural numbers: induction and recursion are two expressions of the same\noperation from lean's point of view.\n\n```\nopen Nat\nexample (n : Nat) : n < succ n := by\n induction n with\n | zero =>\n show 0 < 1\n decide\n | succ i ih => -- ih : i < succ i\n show succ i < succ (succ i)\n exact Nat.succ_lt_succ ih\n```\n\nThis type is special-cased by both the kernel and the compiler:\n* The type of expressions contains \"`Nat` literals\" as a primitive constructor,\n and the kernel knows how to reduce zero/succ expressions to nat literals.\n* If implemented naively, this type would represent a numeral `n` in unary as a\n linked list with `n` links, which is horribly inefficient. Instead, the\n runtime itself has a special representation for `Nat` which stores numbers up\n to 2^63 directly and larger numbers use an arbitrary precision \"bignum\"\n library (usually [GMP](https://gmplib.org/)).\n",
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": "\n | ",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": {"type": "Nat", "name": "0", "_type": "typeinfo"},
"semanticType": null,
"raw": "0",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": " => ",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": {"type": "Nat", "name": "0", "_type": "typeinfo"},
"semanticType": null,
"raw": "0",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": "\n | ",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": {"type": "Nat", "name": "n", "_type": "typeinfo"},
"semanticType": "Name.Variable",
"raw": "n",
"link": null,
"docstring": null,
"_type": "token"},
{"typeinfo": null,
[{"typeinfo": null,
"semanticType": null,
"raw": " + 1 => ",
"raw": "example : Nat → Nat\n | 0 => 0\n | n + 1 => ",
"link": null,
"docstring": null,
"_type": "token"}],
Expand All @@ -82,11 +14,10 @@
"_type": "goal"}],
"contents":
[{"typeinfo": null,
"semanticType": "Keyword",
"semanticType": null,
"raw": "by",
"link": null,
"docstring":
"`by tac` constructs a term of the expected type by running the tactic(s) `tac`. ",
"docstring": null,
"_type": "token"}],
"_type": "sentence"},
{"messages": [],
Expand All @@ -101,8 +32,7 @@
"semanticType": null,
"raw": " ",
"link": null,
"docstring":
"`by tac` constructs a term of the expected type by running the tactic(s) `tac`. ",
"docstring": null,
"_type": "token"}],
"_type": "sentence"},
{"messages": [],
Expand All @@ -113,22 +43,8 @@
"_type": "goal"}],
"contents":
[{"typeinfo": null,
"semanticType": "Keyword",
"raw": "exact",
"link": null,
"docstring":
"`exact e` closes the main goal if its target type matches that of `e`.\n",
"_type": "token"},
{"typeinfo": null,
"semanticType": null,
"raw": " ",
"link": null,
"docstring":
"`exact e` closes the main goal if its target type matches that of `e`.\n",
"_type": "token"},
{"typeinfo": {"type": "Nat", "name": "n", "_type": "typeinfo"},
"semanticType": "Name.Variable",
"raw": "n",
"raw": "exact n",
"link": null,
"docstring": null,
"_type": "token"}],
Expand Down
Loading

0 comments on commit 616aca4

Please sign in to comment.