unison/unison-src/transcripts/any-extract.output.md
Greg Pfeil 0031542faf
Add a space before code block info strings
This is for consistency with the `cmark` style. Now the blocks we still
pretty-print ourselves will match the bulk of them that `cmark`
produces.
2024-07-10 13:56:07 -06:00

42 lines
1.0 KiB
Markdown

# Unit tests for Any.unsafeExtract
Any.unsafeExtract is a way to extract the value contained in an Any. This is unsafe because it allows the programmer to coerce a value into any type, which would cause undefined behaviour if used to coerce a value to the wrong type.
``` unison
test> Any.unsafeExtract.works =
use Nat !=
checks [1 == Any.unsafeExtract (Any 1),
not (1 == Any.unsafeExtract (Any 2)),
(Some 1) == Any.unsafeExtract (Any (Some 1))
]
```
``` ucm
Loading changes detected in scratch.u.
I found and typechecked these definitions in scratch.u. If you
do an `add` or `update`, here's how your codebase would
change:
⍟ These new definitions are ok to `add`:
Any.unsafeExtract.works : [Result]
Now evaluating any watch expressions (lines starting with
`>`)... Ctrl+C cancels.
3 | checks [1 == Any.unsafeExtract (Any 1),
✅ Passed Passed
```
``` ucm
scratch/main> add
⍟ I've added these definitions:
Any.unsafeExtract.works : [Result]
```