inductive type with no base case is a constant ?

Stream: general

[Anatole Dedecker]

Why are docs#false and docs#empty marked as constants in the docs (including the scary red box) although they are just innocent inductive types ?

[Patrick Massot]

Every inductive type adds constant to the environment.

[Patrick Massot]

Those constant aren't listed in the docs usually, but I guess in those two cases there is nothing else to list since there are no constructors.

[Anatole Dedecker]

Oh indeed that makes sense. Thanks !

[Patrick Massot]

You run

run_cmd
do env ← tactic.get_env,
   decl ← env.get `nat,
   tactic.trace decl.is_constant,
   tactic.skip

run_cmd
do env ← tactic.get_env,
   decl ← env.get `nat.rec,
   tactic.trace decl.is_constant,
   tactic.skip

and put your cursor on each run_cmd to see that both nat and nat.recare constants.

[Patrick Massot]

The calculus of inductive construction is a huge machine to create mathematical objects from nowhere. When defining nat you are postulating the existence of a type with its constructors and recursor, coming out of nowhere, so you get constants everywhere.

[Patrick Massot]

This is very different from set theoretical foundations where the rule of the game is that everything must be a set, constructed using a handfull of allowed formulas, and you need tricks to encode everything (see eg https://en.wikipedia.org/wiki/Natural_number#Constructions_based_on_set_theory)

[Anatole Dedecker]

Yep that makes total sense now, thanks again. On the topic of esoteric set theory constructions, I'm a big fan of this one https://en.wikipedia.org/wiki/Ordered_pair#Defining_the_ordered_pair_using_set_theory

[Patrick Massot]

Yes, it's the same issue. And note that functions in set theory are defined as sets of pairs (their graphs), so things like this pile up.