/usr/share/hol88-2.02.19940316/help/ENTRIES/outl.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 outl
\TYPE {outl : ((* + **) -> *)}
\SYNOPSIS
Projects out of left summand.
\DESCRIBE
The function {outl} is associated with the disjoint union
construction of types. It projects out of the left summand of the union.
\FAILURE
Fails if the operand is a right summand.
\EXAMPLE
{
#let x = inl 1
#and y = inr 2;;
x = inl 1 : (int + *)
y = inr 2 : (* + int)
#outl x;;
1 : int
#outl y;;
evaluation failed outl
}
\SEEALSO
outr inl inr isl.
\ENDDOC
|