prelude

structure And where
  left : Type
  right : Type

#check And
        --^ completion
#check And.
         --^ completion