Skip to main content

Typeclasses and Generic Inductive Types

Kevin Lacker
Generalist

Since launching the Acorn beta, we've heard consistent feedback from mathematicians that they need a powerful type system to represent their favorite area of mathematics.

Today, we're releasing two big improvements to Acorn's type system. The first is typeclasses.

The Build Cache

Kevin Lacker
Generalist

There's a useful new feature in Acorn Prover 0.0.8: a build cache.

When you save changes to an Acorn project, the AI model automatically completes simple proofs with missing steps. Usually this works great, but this can make refactoring more difficult. In particular, if you make changes to a module like nat.ac that many other modules depend on, it can be slow to rebuild everything. If you want to remove a theorem that is used in many places, this can involve many slow rebuilds.

Generics

Kevin Lacker
Generalist

We've deployed a new version of the Acorn Prover, 0.0.5, with support for a commonly requested feature: generic types. For example, the standard library now has a Pair structure:

structure Pair<T, U> {
first: T
second: U
}

Hello World

Kevin Lacker
Generalist

Good news, everybody!

With this blog post, I hereby demonstrate that the Acorn blog is now capable of handling posts.