#  Some proofs should be easy. Some programs should be easy.
#  The easiest proofs are of things that are obviously true.
#  The "void" value " " is obvious. It carries no information.

(( :True) be (\@b->b))

#  If this is your first program in Ambidexter, some explanation is in order.
#  All these lines beginning with # are comments.
#  ( :True) is the part we're interested in.
#  Parentheses ( ) are for grouping just as in mathematics.
#  :True is a "type annotation". It tells the type of the term to its left.

#  The space in ( :True) is the term. There's nothing to it!
#  It supplies no information, because no information is needed in
#  a proof of something that's inherently True.

#  The phrase "be (\@b->b)" serves to form a complete program around
#  the ( :True) term.  The point of an Ambidexter program is to describe
#  "what to do". ( :True) is not a program because it doesn't do anything.
#  Adding "be (\@b->b)" says what to do, namely to make the value
#  ( :True) available but to make no use of it.

#  "be (\@b->b)" uses some more advanced features of the language which
#  will be explained later.