why do declarations with unknown types compile?

Stream: new members

[JJ]

to my surprise, the following code compiles, despite Foo not being defined anywhere:

def foo : Foo := sorry

what is this useful for? it strikes me as very counterintuitive behavior, so i suspect there's probably a reason for it.

[Bjørn Kjos-Hanssen]

Similarly you can do

example : x = Real.pi := sorry

and Lean will infer that x must be a real number it hasn't seen before, and you're trying to prove it's equal to pi.

I think the philosophy is that if you can prove something about Foo without saying what it is, then you've proved it for all Foo, in this case for all Foo : Sort u_1 (which you can see by hovering over Foo in your code).

[Kevin Buzzard]

If we're talking about autoimplicits, you can disable them with set_option autoImplicit false. Mathlib does this globally in the lakefile.

[JJ]

hmm, i think this might be separate from autoimplicits? the manual says the following:

When Lean processes the header of a declaration, any unbound identifier is automatically added as an implicit argument if it is a single lower case or greek letter.

this isn't the case for the example above. maybe lean's behavior has changed and the manual wasn't updated?

[Damiano Testa]

I think that the single identifiers autoimplicits became relaxedAutoImplicits. autoImplicits are all of them, no restrictions.