## Stream: new members

### Topic: application at variables

#### Horatiu Cheval (Feb 26 2021 at 13:58):

How can I apply terms to variables in defs (or create variables defined respectively to other variables, so to say), in the following sense?

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare variables for some of its arguments
variables {X : Type} (a₀ : X)
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type ℕ → α
def x := seq a₀

#check x
-- but it still has type ?M_1 → ℕ → ?M_1


#### Kevin Buzzard (Feb 26 2021 at 14:09):

That's because a variable is not actually a variable in the sense that it's defined once and for all, for the rest of the file -- a variable is just a trick whereby in your definition of x Lean thinks "crumbs -- what is a_0? Oh -- I see the user declared it as a variable, so I'll just stick "for all a_0 : X" in that def -- oh crumbs -- what is X? Oh that's a variable too, so I'll just stick "for all {X : Type}" in as well"

#### Kevin Buzzard (Feb 26 2021 at 14:11):

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare constants for some of its arguments
constants {X : Type} (a₀ : X)
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type ℕ → α
noncomputable def x := seq a₀

#check x -- x : ℕ → X


Note that there are no constants in mathlib -- you can easily prove false statements if you start throwing constants around. If you actually know what you want a_0 to be, then let it be that, and if you don't, then actually you might want it as a variable in Lean's sense.

#### Kevin Buzzard (Feb 26 2021 at 14:13):

If you really don't want variables then this is safer than using constants:

-- I have a general definition like this
def seq : ∀ {α : Type} (a : α), ℕ → α := sorry
-- then I declare sorried definitions for some of its arguments
def X : Type := sorry
def a₀ : X := sorry
-- now I want to consider seq partially applied at a₀,
-- so that I get something of type ℕ → α
def x := seq a₀

#check x -- x : ℕ → X


This time Lean emits a warning saying that you cheated, so proofs of false are known not to be trusted.

#### Horatiu Cheval (Feb 26 2021 at 14:20):

Thanks for the insight on how variables work! I knew defining constants is not recommended, plus it doesn't seem to represent the intention. Essentially, I defined some sorts of recursive sequences, having the initial value as argument, and then I wanted to have an initial point and a sequences starting at that point as variables, to reduce verbosity.

def seq : ∀ {α : Type} (a : α), ℕ → α := sorry

variables {X : Type} (a₀ : X)

local notation x := seq a₀

#check x


I guess this works best, but reserving the token x didn't seem the best idea.

#### Eric Wieser (Feb 26 2021 at 16:58):

parameters {X : Type} {a₀ : X} may work for you too

Last updated: May 15 2021 at 02:11 UTC