| Mode | Name | Size | |
|---|---|---|---|
| -rw-r--r-- | .gitignore | 7 | logplainblame |
| -rw-r--r-- | BinaryHeap.lean | 3589 | logplainblame |
| d--------- | BinaryHeap | 130 | logplain |
| -rw-r--r-- | LICENSE | 1070 | logplainblame |
| -rw-r--r-- | README.md | 2109 | logplainblame |
| -rw-r--r-- | TODO | 1625 | logplainblame |
| -rw-r--r-- | lake-manifest.json | 116 | logplainblame |
| -rw-r--r-- | lakefile.lean | 105 | logplainblame |
| -rw-r--r-- | lean-toolchain | 22 | logplainblame |
 |
index : BinaryHeap | |
| A toy project about formal validation of a Heap in Lean4 | Andreas Grois |
| aboutsummaryrefslogtreecommitdiff |