lthms ⸮ is a user on mastodon.social. You can follow them or interact with them if you have an account anywhere in the fediverse.
If you don't, you can sign up here.
Discovery of the day.
`Inductive False: Prop.` is a valid #coq construction, and it creates one constructor for `False` whereas `Inductive False: Prop :=.` is *also* a valid construction, and it does not create a constructor by default (meaning `False` is empty in this case).
