/usr/share/hol88-2.02.19940316/help/ENTRIES/inl.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 | \DOC inl
\TYPE {inl : (* -> (* + **))}
\SYNOPSIS
Injects into left of disjoint union type.
\DESCRIBE
The function {inl} is a constructor function for disjoint union (sum) types,
which takes an element of an arbitrary type {*} and creates an element of type
{* # **} which holds the same data.
\FAILURE
Never fails
\EXAMPLE
{
#let x = inl 1;;
x = inl 1 : (int + *)
#let y = inl `hello` : string + int;;
y = inl `hello` : (string + int)
}
\SEEALSO
inr, isl, outl, outr.
\ENDDOC
|