yes_or_no : type.
yes : yes_or_no.
no : yes_or_no.

rec andalso : ( ⊢ yes_or_no) → ( ⊢ yes_or_no) → ( ⊢ yes_or_no) =
fn x ⇒ fn y ⇒ case x of
              | [ ⊢ no] ⇒ [ ⊢ no]
              | [ ⊢ yes] ⇒ y;

© Computation and Logic Group
Department of Computer Science, McGill University
3480 University Street, Montreal, Quebec, Canada, H3A 0E9