summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ScalarNotations.lean (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Fix more issues with the scalar notationsSon Ho2024-06-131-15/+29
|
* Fix more issuesSon Ho2024-06-131-14/+19
|
* Add an exampleSon Ho2024-06-121-0/+3
|
* Update the scalar notations in LeanSon Ho2024-06-121-0/+87