summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives/ScalarNotations.lean (unfollow)
Commit message (Expand)AuthorFilesLines
2024-06-13Fix more issues with the scalar notationsSon Ho1-15/+29
2024-06-13Fix more issuesSon Ho1-14/+19
2024-06-12Add an exampleSon Ho1-0/+3
2024-06-12Update the scalar notations in LeanSon Ho1-0/+87