Supertype is an extension of lean's Subtype
that provides addional conveniences, features and syntax.
To get started, add the following line to your lakefile.lean
.
require supertype from git "https://github.com/somombo/supertype" @ "main"
At the top of every lean file where you want to use Supertypes, add:
import Supertype
Then you can use the package in the following manner:
def x : { // 5 + · < 17 } := 2 ...
def y : { (a, b) // 5 ≤ a + b } := ... (4,3)
(For more examples of usage and syntax,
See Examples.lean
file)