prelude

set_option relaxedAutoImplicit false
inductive Foo where
 | bar : F
        --^ completion