Skip to content

Instantly share code, notes, and snippets.

@podikoglou
Created July 1, 2025 10:30
Show Gist options
  • Save podikoglou/8a155d1fbbd26d6bd3c9bd7e24f2d06a to your computer and use it in GitHub Desktop.
Save podikoglou/8a155d1fbbd26d6bd3c9bd7e24f2d06a to your computer and use it in GitHub Desktop.

My Notes on Lean4

Types

A few basic types are:

  • Bool
  • Nat
  • Float

Constants

You define constants with the following syntax:

def j : Nat = 3
def k : Bool = false

Commands

There's some auxiliary commands such as:

  • #check: which type checks an expression
  • #eval: which evaluates an expression

These are ways of interacting with the system.

Fun Discovery with Type Checking

The Bool type seems to have two values: true and false. That makes sense. However when playing with #check I accidentally typed True instead of true and noticed that it's not invalid, and True is in fact of type Prop. That's fascinating and makes quite a lot of sense. It's an atomic proposition which always takes the value true, and of course, False exists too. Fun!

On typing weird symbols

I have not yet tried using Lean with neovim, but from the browser version (which uses monaco and bundles Lean's extension, I suppose), typing symbols like ∧ seems to work in a way similar to LaTeX, you type \and (notice: it's not \land but \and, for some reason. I mean, it makes sense: you don't have other and symbols, but it kills muscle memory.). Further note: you can also use && (and is so far preferred by the book)

Functions

Typing

Let a and b be types. A function from a to b (i.e. a function that takes an input of type a and returns one of type b), is typed a → b.

def a := Nat
def b := Nat

#check a -> b -- a → b : Type

(1: the : Type part seems to be the...type of the type? or well, the type of the return value of #check maybe, but I might be wrong)

(2: YES! types are first class citizens, seemingly. so, you can make constants which are types. FUN!!!)

Need more inputs? Cartesian product. Observe:

a × b -> c

The above is the type of a function that takes two inputs, one of type a and one of type b, and returns an output of type c. The strikethrough above is actually what you may perceive it as, but it's not accurate:

The above is the type of a function which takes a single input and returns a single output. The input's type is a ordered pair, where the first element is of type a and the second is of type b. The output is of type c.

Expanding on my curiosity: can a function return a type?

def a := Nat
def b := Nat
def c := (a × b) -> Type

#check c -- Type 1

ooh. Yeah, I don't know what that means, but it's not erroring... so..... yes?...

Infix operators?

Prod

Don't wanna write a × b? You can just.......... use an .... sigh infix operator called Prod. Observe:

#check a × b    -- a × b : Type
#check Prod a b -- a × b : Type

Fun question to ask: is this an operator or a function? (or both? although that's more of a philosophical question)

Funner quesetion to ask: how could we craft a proposition that determines whether two objects -- in our case, types -- are equal? This would simplify the above text into one line which would output true or false, showing whether the two syntaxes are equivalent.

Some more stuff on Pairs

I had forgotten that this is not just types... you can have values, and you can have values that are pairs. Silly me. Here's a pair:

#check (1, 3.5) -- Nat × Float

Flattened?

I'm sure this makes loads of sense but I can't quite wrap my head aroudn this right now:

#check (3, (3, (3, (3, (3, (3)))))) -- (3, 3, 3, 3, 3, 3) : Nat × Nat × Nat × Nat × Nat × Nat

Access

#eval (5, 9).1 -- 5

There's also .fst and .snd

Nat.succ

#check Nat.succ

What type do you think this returns? Nat -> Nat? Yeah, that's what I'd think. Hell, just to be nice I'd say Nat -> Nat : Type.

But noooooooo, it's (n : Nat) : Nat.

My understanding is that for some stupid reason n here is the name of the input, which is useless on the type level. Nat (the first one) is the type of the input, that makes sense. And Nat (the alst one) is the return type? BUT WHAT HAPPENED TO ->?!?!?!

The good thing is that if you let Lean interpret this, it will say

Expected type: ⊢ Nat → Nat

Which is good, but leaves questions about what #check really does.

Computing Succ

Hey, okay, here it is:

#check Nat.succ 4 -- Nat.succ 4 : Nat

Yeah, makes sense, I suppose, but wait a minute hold on. Why is Nat.succ 4 there? uhhhhhhhhhhhhhhhh. Wait, how does this link back to my previous rant?

Could it, perhaps, be there for the same reason (n: Nat) was there? ohhhh, right. For whatever reason n is named (perhaps I can do that with Nat.succ 4 here as welll) and it's just... telling me the type, but in a weird way. I truly don't now what it gives me still though.

Functions that return functions and currying

#check Nat → Nat → Nat -- Nat → Nat → Nat : Type

This is slang for, a function that takes a Nat and returns a funciton that takes a Nat and returns a Nat. Even though I knew of the concept of currying and expected it to be here I had trouble with this, but it makes sense now.

The reason I had trouble is because, why the hell do we have two mechanisms of providing more than one input to a function? we have ordered pairs, and now we have currying. They achieve the same thing, but in different ways, right? and well, currying has a lot more applications and general advantages, too.

Nat.Add

Behold, Nat.Add.

#check Nat.add     -- Nat.add     : Nat → Nat → Nat
#check Nat.add 3 1 -- Nat.add 3 1 : Nat
#check Nat.add 3   -- Nat.add 3   : Nat → Nat

I love currying, actually. So, when you provide one argument, it removes one level of the function chain, sorta.

Type Hierarchy

That's a word I came up with, don't quote me.

Some expanding on the type system and how types are first class citizens:

#check Bool -- Bool : Type

Notice how Bool, a type, is of type... Type!

And of course,

#check Type -- Type : Type 1

What happens when you

#eval Bool
```?

I like the error message, it reads:

cannot evaluate, types are not computationally relevant


Oh yeah, remember `Prod` from earlier? you're not gonna believe this, but it's
a ~~function~~, and operates on types. HELL YES!

#check Prod -- Prod.{u, v} (α : Type u) (β : Type v) : Type (max u v)


NOTE: I have read further and at this point... I don't know if it's a
function... (maybe a parametrized type of sorts?)

Okay that's big to unpack, I'll check on it later and see if I get it then.

Basically my point is that the type is actually `Type -> Type -> Type`.

You can check this by creating a constant of which you explicitly define the
type rather than letting Lean infer it, and setting its value to `Prod`! If it
errors, you're wrong. If it doesn't, ding ding ding!
```lean
def P : Type -> Type -> Type := Prod -- No errors!

Lists!

List is a type which from what I understand takes a type parameter of sorts. That, or it's a function that returns a type. That's the approach Zig takes from what I gather, and I think it's quite clean! Not sure which one it is though.

Anyway.

def NatList := List Nat

#check NatList -- NatList : Type

Type Universes

Gosh that's a beautiful concept.

Earlier I stumbled upon the fact that Type is of type Type 1. Turns out that Type 1 is of type Type 2, which is of type Type 3, and so on, until... not sure, but it's infinite.

Type 0 is a universe of, from what I gather, simple types.

Type 1 is larger, and contains Type 0 as an element!

Naturally, Type 2 is even larger and contains Type 1 as an element.

Type is an abbreviation of Type 0

So, every Type n is of type Type n+1.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment