summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ScalarNotations.lean (follow)
Commit message (Expand)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