Yatima.ContAddr

This module is responsible for content-addressing the constants from a Lean.Environment, which contains the data extracted from a parsed Lean 4 source file.

By "content-addressing" we mean to extract the essential name-irrelevant information from a Lean constant. To illustrate it, let's consider the following inductive types:

inductive Nat | zero | succ : Nat → Nat
inductive Cat | nope | next : Cat → Cat

Even though Nat and Cat are different types with different constructors, they have the same structure:

• No arguments
• The first constructor has no arguments
• The second constructor has one argument... a term of itself
• No other constructor

Thus, if we strip their names, we expect to end up with the same anonymized data, whose hash should coincide.

Nats and cats are different, but equal!?

If Nat and Cat are content-addressed to the same Yatima IR but, in Lean, they are not the same thing, does that create a soundness breach that would allow a proof of False in the Yatima typechecker?

[TODO]

Yatima IR

The datatypes used to capture anonymized constants are what we refer to by Yatima intermediary representation (IR) types. And since we have to reflect Lean's expressiveness, these are the Yatima IR types:

TODO: explicit Yatima.IR.Univ, Yatima.IR.Expr and Yatima.IR.Const

Content-addressing universe levels

[easy]

Content-addressing expressions

[easy, but there's a trick involving the use of Expr.var to denote recursive calls]

Content-addressing constants

[this section is rather involved]

Straightforward constants

Mutual blocks

Definitions

Inductive types

Hashing