I have the following goal:

⊢ ∃ δ, 0 < δ ∧ ∀ (x : ℝ), 0 < x - 0 ∧ x - 0 < δ → M < f x

I am curious and want to see how the propositional constructors are applied to my expressions (especially AND and IMPLIES and perhaps EXSITS) e.g., I want to know if it's Implies( And( Exists(delta, delta > 0), ∀ (x : ℝ), 0 < x - 0 ∧ x - 0) , M < f x or something else. Can I have Lean4 show this info to me, at least temporarily?

I tried it the following:

Hover over an operator in the info view and it will highlight the arguments passed to that operator. Alternatively try setting some option like pp.notation (see https://leanprover.github.io/reference/other_commands.html#options) to false.

but it didn't work for forall and I think also it didn't work for implies (it did for exists) see:

enter image description here

enter image description here

In addition, I don't understand. I am trying to click the forall definition or the implication, but it doesn't take me to either in vscode. Why doesn't it work for those? I assumed perhaps forall is defined in terms of exists but even if that was the case I should be able to see it's declaration/definition.

  • $\begingroup$ Forall and implication are built into the logic of dependent type theory. They aren’t defined. Implication, forall, function types, and Pi types are represented internally as the same thing. P -> Q is the same as \forall (h : P), Q, which is the same as (h : P) -> Q. In other words it is the type of functions which take proofs of P and return proofs of Q. $\endgroup$
    – Jason Rute
    Commented Mar 2 at 2:57
  • $\begingroup$ Also, in Lean (and most other theorem provers) binders bind very loosely (unlike some logic textbooks), so the statement is EXISTS ( AND (0 < delta, FORALL ( IMPLIES ( AND (…,…), …))). This is more natural from a mathematical perspective (where most theorems are forall theorems. $\endgroup$
    – Jason Rute
    Commented Mar 2 at 4:27
  • $\begingroup$ In case you more familiar with Coq, most everything is the same in these above regards as Coq. $\endgroup$
    – Jason Rute
    Commented Mar 2 at 4:29
  • $\begingroup$ I'm also really confused by your question. When you hover over for it does show the correct scope of the operator, and you can even see that for in your image. $\endgroup$
    – Jason Rute
    Commented Mar 2 at 16:55

1 Answer 1


After reading this question many times, I think the main question is as follows:

Why do implications and forall behave differently from other notations, for example in the info-view hover feature, the click-through to see the definition, and print settings like set_option pp.notation false/set_option pp.all true?

As I state in my comment above, implication and forall are special in dependent type theory. They are not defined, but instead built into the logic itself. They are just instances of dependent function types (Pi types). An implication p -> q can be thought of as the type of functions which take "proofs" of p to "proofs" of q. Similarly, ∀ (x : A), r x can be thought of as the type of dependent functions which take x : A to a "proof" of r x. Lean prints the term with one of three notations depending on circumstance, but they are all internally represented the same as the following examples show:

import Mathlib

-- logical implication
axiom p : Prop
axiom q : Prop
#check p → q         -- p → q : Prop
#check ∀ (a : p), q  -- p → q : Prop
#check Π (a : p), q  -- p → q : Prop
#check (a : p) → q   -- p → q : Prop
theorem ex1 (a : p) : q := sorry
#print ex1           -- theorem ex1 : p → q

-- function types
axiom A : Type
axiom B : Type
#check A → B         -- A → B : Type
#check ∀ (a : A), B  -- A → B : Type
#check Π (a : A), B  -- A → B : Type
#check (a : A) → B   -- A → B : Type
def ex2 (a : A) : B := sorry
#print ex2           -- def ex2 : A → B

-- forall
axiom r : A -> Prop
#check ∀ (x : A), r x  -- ∀ (x : A), r x : Prop
#check Π (x : A), r x  -- ∀ (x : A), r x : Prop
#check (x : A) → r x   -- ∀ (x : A), r x : Prop
theorem ex3 (x : A) : r x := sorry
#print ex3             -- theorem ex3 : ∀ (x : A), r x

-- dependent function types
axiom C : A -> Type
#check ∀ (x : A), C x  -- (x : A) → C x : Type
#check Π (x : A), C x  -- (x : A) → C x : Type
#check (x : A) → C x   -- (x : A) → C x : Type
def ex4 (x : A) : C x := sorry
#print ex4             -- def ex4 : (x : A) → C x

Now, it is also probably true Lean 4 could be better at conveying this information in the hovers, info view, and print settings. There is no print setting I know of which prints these all the same.

Also, you mention forall or exists being defined in terms of the other. This is common in classical first order logic, but it isn't generally true of dependent type theory (even dependent type theory with classical logic). There are many advantages of defining forall and exists in the way Lean does, where Exists is defined as a structure and forall is a Pi type.

I highly recommand the first four sections of Theorem Proving in Lean 4 for an explanation on this.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.