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

chore: fix test output

Browse source
This commit is contained in:
Leonardo de Moura 2022-08-04 15:29:17 -07:00
parent 8615c42a5d
commit f295a76b69
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
tests/lean/interactive/hover.lean.expected.out
View file

@ -247,5 +247,5 @@ null
"end": {"line": 172, "character": 32}},
"contents":
{"value":
"```lean\nId Nat\n```\n***\nTry to expand `·` notation.\nRecall that in Lean the `·` notation must be surrounded by parentheses.\nWe may change this is the future, but right now, here are valid examples\n- `(· + 1)`\n- `(f ⟨·, 1⟩ ·)`\n- `(· + ·)`\n- `(f · a b)` ",
"```lean\nId Nat\n```\n***\nYou can use parentheses for\n- Grouping expressions, e.g., `a * (b + c)`.\n- Creating tuples, e.g., `(a, b, c)` is notation for `Prod.mk a (Prod.mk b c)`.\n- Performing type ascription, e.g., `(0 : Int)` instructs Lean to process `0` as a value of type `Int`.\n- Creating `Unit.unit`, `()` is just a shorthand for `Unit.unit`.\n- Creating simple functions when combined with `·`. Here are some examples:\n - `(· + 1)` is shorthand for `fun x => x + 1`\n - `(· + ·)` is shorthand for `fun x y => x + y`\n - `(f · a b)` is shorthand for `fun x => f x a b`\n - `(h (· + 1) ·)` is shorthand for `fun x => h (fun y => y + 1) x`\n",
"kind": "markdown"}}