Are these two styles completely equivalent?

Stream: new members

[Dan Abramov]

  have hfn : ∀ {i}, ∀ s : S i, f s n' = i := by
    intro i s
    -- ...

vs

  have hfn {i} (s : S i) : f s n' = i := by
    -- ...

Is there any differences between these at all from the outside perspective? Or are they 100% equivalent?

[Aaron Liu]

in all normal cases these do the exact same thing

[Aaron Liu]

I can think of one case where I think these will be different

[Dan Abramov]

From the typesystem's perspective, this is the same type, right? Just different way to format it. Although then I'm not sure how to interpret the fact that ∀ {i}, ∀ s : S i, f s n' = i is also a legit independent thing (of type Prop). Whereas I'm not sure if I can rip out some version of {i} (s : S i) : f s n' = i as a standalone expression, and what type it could have...

[Jakub Nowak]

Does hfn (s := smth) works with the first one?

[Dan Abramov]

Jakub Nowak said:

Does hfn (s := smth) works with the first one?

Yup, works with both.

[Yakov Pechersky]

The former requires an intro tactic step to introduce the variables. You might not want that if the step is to apply a recursor.

[Ruben Van de Velde]

The second is just syntax for the former, just like theorem fn {i} (s : S i) : f s n' = i := sorry is syntax for theorem fn : \forall...

[Dan Abramov]

Ruben Van de Velde said:

The second is just syntax for the former

In my mind, theorem itself is syntax sugar for something like noncomputable def; wouldn't this mean that normal argument lists in def are also syntax sugar for ∀? I guess I was expecting currying to be the primary primitive.

[Lawrence Wu (llllvvuu)]

IIUC noncomputable def can be used to define data, even if the data is uncomputable, but theorem can’t be used to define data at all

[Aaron Liu]

tada

set_option pp.proofs true
set_option pp.mvars false

/--
trace: case h
u n' : Nat
S : Nat → Type
f : {i : Nat} → S i → Nat → Nat
kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat
ss : S u
⊢ kc u ss n'
      (have hfn := fun {i} => ?_;
      hfn ss) =
    0

case c
u n' : Nat
S : Nat → Type
f : {i : Nat} → S i → Nat → Nat
kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat
ss : S u
⊢ ∀ (i : Nat) (s : S i), f s n' = i
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (u n' : Nat) (S : Nat → Type) (f : {i : Nat} → S i → Nat → Nat)
    (kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat)
    (ss : S u) :
    (∀ i (s : S i), f s n' = i) ∧ ∃ hn, kc u ss n' hn = 0 := by
  refine ⟨?c, ?n, ?h⟩
  rotate_left
  have hfn : ∀ {i}, ∀ s : S i, f s n' = i := by
    intro i s
    exact ?c i s
  exact hfn ss
  trace_state
  all_goals sorry

/--
trace: case h
u n' : Nat
S : Nat → Type
f : {i : Nat} → S i → Nat → Nat
kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat
ss : S u
⊢ kc u ss n'
      (have hfn := fun {i} s => ?_;
      hfn ss) =
    0

case c
u n' : Nat
S : Nat → Type
f : {i : Nat} → S i → Nat → Nat
kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat
ss : S u
⊢ ∀ (i : Nat) (s : S i), f s n' = i
---
warning: declaration uses 'sorry'
-/
#guard_msgs in
example (u n' : Nat) (S : Nat → Type) (f : {i : Nat} → S i → Nat → Nat)
    (kc : (i : Nat) → (s : S i) → (n : Nat) → f s n = i → Nat)
    (ss : S u) :
    (∀ i (s : S i), f s n' = i) ∧ ∃ hn, kc u ss n' hn = 0 := by
  refine ⟨?c, ?n, ?h⟩
  rotate_left
  have hfn {i} (s : S i) : f s n' = i := by
    exact ?c i s
  exact hfn ss
  trace_state
  all_goals sorry

[Aaron Liu]

yeah it's really not a very big difference