niubie

Stream: new members

[hule]

i have known lean for few days. Can somebody help me to understand why "C" is wrong but "c" is correct in below code.
Screenshot 2025-06-06 135018.png

[Rémy Degenne]

It's perhaps easier to understand if you replace C with Nat, the natural numbers. You want a function from the natural numbers to the natural numbers. So if c is in Nat, returning c is indeed returning a natural number, and fun c : Nat => c is a valid function Nat -> Nat.
But what you are doing is taking c : Nat and returning the type Nat. Nat is not itself a natural number, it's the type of natural numbers, so you are not defining a function Nat -> Nat.

[hule]

I get it, thank you.