mirror of
https://github.com/unisonweb/unison.git
synced 2024-09-17 13:27:30 +03:00
Transcript output
This commit is contained in:
parent
1d7468e12a
commit
3457a4b9c8
@ -86,21 +86,17 @@ ex4 =
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I couldn't find any definitions matching the name a inside the namespace .
|
||||
I couldn't figure out what a refers to here:
|
||||
|
||||
2 | (a,b) = (a Nat.+ b, 19)
|
||||
|
||||
Its type should conform to Nat .
|
||||
Some common causes of this error include:
|
||||
* Your current namespace is too deep to contain the
|
||||
definition in its subtree
|
||||
* The definition is part of a library which hasn't been
|
||||
added to this project
|
||||
|
||||
To add a library to this project use the command: `fork <.path.to.lib> .lib.<libname>`
|
||||
|
||||
Whatever it is, its type should conform to Nat.
|
||||
|
||||
|
||||
* You have a typo in the name
|
||||
|
||||
```
|
||||
Even though the parser accepts any pattern on the LHS of a bind, it looks pretty weird to see things like `12 = x`, so we avoid showing a destructuring bind when the LHS is a "literal" pattern (like `42` or "hi"). Again these examples wouldn't compile with coverage checking.
|
||||
|
@ -194,9 +194,10 @@ Note that because of the special treatment of the first line mentioned above, wh
|
||||
|
||||
doc3 : Doc
|
||||
doc3 =
|
||||
[: When Unison identifies a paragraph, it removes any newlines
|
||||
from it before storing it, and then reflows the paragraph text
|
||||
to fit the display window on display/view/edit.
|
||||
[: When Unison identifies a paragraph, it removes any
|
||||
newlines from it before storing it, and then reflows the
|
||||
paragraph text to fit the display window on
|
||||
display/view/edit.
|
||||
|
||||
For these purposes, a paragraph is any sequence of non-empty
|
||||
lines that have zero indent (after the unindenting mentioned
|
||||
@ -209,8 +210,8 @@ Note that because of the special treatment of the first line mentioned above, wh
|
||||
is not treated | either.
|
||||
|
||||
Note that because of the special treatment of the first line
|
||||
mentioned above, where its leading space is removed, it is always
|
||||
treated as a paragraph.
|
||||
mentioned above, where its leading space is removed, it is
|
||||
always treated as a paragraph.
|
||||
:]
|
||||
|
||||
```
|
||||
@ -401,24 +402,25 @@ para line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolo
|
||||
|
||||
test1 : Doc
|
||||
test1 =
|
||||
[: The internal logic starts to get hairy when you use the \@
|
||||
features, for example referencing a name like @List.take. Internally,
|
||||
the text between each such usage is its own blob (blob ends here
|
||||
--> @List.take), so paragraph reflow has to be aware of multiple
|
||||
blobs to do paragraph reflow (or, more accurately, to do the
|
||||
normalization step where newlines with a paragraph are removed.)
|
||||
[: The internal logic starts to get hairy when you use the
|
||||
\@ features, for example referencing a name like @List.take.
|
||||
Internally, the text between each such usage is its own blob
|
||||
(blob ends here --> @List.take), so paragraph reflow has to
|
||||
be aware of multiple blobs to do paragraph reflow (or, more
|
||||
accurately, to do the normalization step where newlines with
|
||||
a paragraph are removed.)
|
||||
|
||||
Para to reflow: lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem
|
||||
ipsum dolor ending in ref @List.take
|
||||
Para to reflow: lorem ipsum dolor lorem ipsum dolor lorem
|
||||
ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor ending in ref @List.take
|
||||
|
||||
@List.take starting para lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor.
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem
|
||||
ipsum dolor lorem ipsum dolor.
|
||||
|
||||
Middle of para: lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor @List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor.
|
||||
Middle of para: lorem ipsum dolor lorem ipsum dolor lorem
|
||||
ipsum dolor @List.take lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor.
|
||||
|
||||
- non-para line (@List.take) with ref @List.take
|
||||
Another non-para line
|
||||
@ -426,22 +428,22 @@ para line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolo
|
||||
|
||||
- non-para line with ref @List.take
|
||||
before a para-line lorem ipsum dolor lorem ipsum dolor lorem
|
||||
ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor.
|
||||
ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor.
|
||||
|
||||
- non-para line followed by a para line starting with ref
|
||||
@List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor.
|
||||
@List.take lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor.
|
||||
|
||||
a para-line ending with ref lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor @List.take
|
||||
a para-line ending with ref lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor @List.take
|
||||
- non-para line
|
||||
|
||||
para line lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor
|
||||
para line lorem ipsum dolor lorem ipsum dolor lorem ipsum
|
||||
dolor lorem ipsum dolor lorem ipsum dolor lorem ipsum dolor
|
||||
lorem ipsum dolor lorem ipsum dolor
|
||||
@List.take followed by non-para line starting with ref.
|
||||
|
||||
@[signature] List.take
|
||||
|
@ -128,10 +128,10 @@ We can view it with `docs`, which shows the `Doc` value that is associated with
|
||||
```ucm
|
||||
.builtin> docs List.take
|
||||
|
||||
`List.take n xs` returns the first `n` elements of `xs`. (No need
|
||||
to add line breaks manually. The display command will do wrapping
|
||||
of text for you. Indent any lines where you don't want it to do
|
||||
this.)
|
||||
`List.take n xs` returns the first `n` elements of `xs`. (No
|
||||
need to add line breaks manually. The display command will do
|
||||
wrapping of text for you. Indent any lines where you don't
|
||||
want it to do this.)
|
||||
|
||||
## Examples:
|
||||
|
||||
|
@ -34,21 +34,17 @@ Now, typecheck a file with a reference to `Blah.zonk` (which doesn't exist in th
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I couldn't find any definitions matching the name Blah.zonk inside the namespace .
|
||||
I couldn't figure out what Blah.zonk refers to here:
|
||||
|
||||
2 | > Blah.zonk [1,2,3]
|
||||
|
||||
Its type should conform to [Nat] -> o .
|
||||
Some common causes of this error include:
|
||||
* Your current namespace is too deep to contain the
|
||||
definition in its subtree
|
||||
* The definition is part of a library which hasn't been
|
||||
added to this project
|
||||
|
||||
To add a library to this project use the command: `fork <.path.to.lib> .lib.<libname>`
|
||||
|
||||
Whatever it is, its type should conform to [Nat] -> o.
|
||||
|
||||
|
||||
* You have a typo in the name
|
||||
|
||||
```
|
||||
Here's another example, just checking that TDNR works for definitions in the same file:
|
||||
|
@ -112,23 +112,18 @@ useAmbiguousTerm = ambiguousTerm
|
||||
|
||||
Loading changes detected in scratch.u.
|
||||
|
||||
I couldn't find any definitions matching the name ambiguousTerm inside the namespace .example.resolution_failures
|
||||
I couldn't figure out what ambiguousTerm refers to here:
|
||||
|
||||
1 | useAmbiguousTerm = ambiguousTerm
|
||||
|
||||
Some common causes of this error include:
|
||||
* Your current namespace is too deep to contain the
|
||||
definition in its subtree
|
||||
* The definition is part of a library which hasn't been
|
||||
added to this project
|
||||
The name ambiguousTerm is ambiguous. Its type should conform to:
|
||||
|
||||
To add a library to this project use the command: `fork <.path.to.lib> .example.resolution_failures.lib.<libname>`
|
||||
_
|
||||
|
||||
There are no constraints on its type.
|
||||
I found some terms in scope that have matching names and
|
||||
types. Maybe you meant one of these:
|
||||
|
||||
I found some terms in scope that have matching names and types. Maybe you meant one of these:
|
||||
|
||||
- one.ambiguousTerm : ##Text
|
||||
- two.ambiguousTerm : ##Text
|
||||
one.ambiguousTerm : ##Text
|
||||
two.ambiguousTerm : ##Text
|
||||
|
||||
```
|
||||
|
Loading…
Reference in New Issue
Block a user