Reservoir

crabbo-rave/lean4-Tuple

Extra and extended datatypes for Lean 4

GitHub Link Documentation

Pick a version!

TODO: should show a time axes that allows the users to view, filter and click copy the lakefile config.

README

Soup

Extra and extended datatypes for Lean 4

Use

Go to lakefile.lean and add the git repo to your dependencies:

package PackageName {
  dependencies := #[
    { name := `Soup, src := Source.git "https://github.com/crabbo-rave/Soup.git" "master"}
    ...
  ]
  ...
}

Features

Contains:

  • Heterogeneous Lists
  • Extra List Functions
  • Accessing nth element of Prod
  • Range functionality
  • Unwrapping Fin type
  • Functor instance for Sum