/usr/share/hol88-2.02.19940316/help/ENTRIES/outr.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 | \DOC outr
\TYPE {outr : ((* + **) -> **)}
\SYNOPSIS
Projects out of right summand.
\DESCRIBE
The function {outr} is associated with the disjoint union construction of
types. It projects out of the right summand of the union.
\FAILURE
Fails if the operand is a left summand.
\EXAMPLE
{
#let x = inl 1
#and y = inr 2;;
x = inl 1 : (int + *)
y = inr 2 : (* + int)
#outr x;;
evaluation failed outr
#outr y;;
2 : int
}
\SEEALSO
outl, inl, inr, isl
\ENDDOC
|