why does this inductive compile with no base cases?

Stream: new members

[Quinn]

inductive Metacircuit : Type :=
| Abs : String -> Metacircuit -> Metacircuit
| App : Metacircuit -> Metacircuit -> Metacircuit

I don't know how to construct terms of this type

[Quinn]

shouldn't the termination checker disallow this?

[Eric Paul]

It's perfectly fine to have a type for which you cannot construct any terms. An example of such a type is False. In fact, you can show that having a term of your type means you can construct one of False:

inductive Metacircuit : Type :=
| Abs : String -> Metacircuit -> Metacircuit
| App : Metacircuit -> Metacircuit -> Metacircuit

example : Metacircuit → False := by
  intro m
  induction m with
  | Abs _ _ ih => trivial
  | App _ _ => trivial

[Quinn]

Oh right.

[Quinn]

So there's like a spectrum between failing the termination checker and constructing a proof of false?

[Quinn]

Why not just get rid of the termination checker, and use malformed types to construct proofs of false?

[Quinn]

I had forgotten about constructorless types and how they might relate, so thanks!

[Adomas Baliuka]

Quinn said:

Why not just get rid of the termination checker, and use malformed types to construct proofs of false?

I would think that we want to have non-inhabited types. Sometimes it might be interesting and hard to prove whether a type is inhabited.

Proofs of False should clearly not be allowed. Did I misunderstandil the question?

[Quinn]

Oops! Didn't mean proof of false, meant A->False

[Luigi Massacci]

Constructing terms of type : A -> False is very much allowed, that's what @Eric Paul just did for you