summaryrefslogtreecommitdiff
path: root/backends/lean/Base/Primitives
diff options
context:
space:
mode:
authorSon Ho2023-11-20 22:38:58 +0100
committerSon Ho2023-11-20 22:38:58 +0100
commit5aa37b3a0a539f9ae37a119b9ce7c8dee504125e (patch)
tree90b8c741f08649c1e017692cf0fc9e1e1c8e402a /backends/lean/Base/Primitives
parent672ceef25203ebd5fcf5a55e294a4ebfe65648d6 (diff)
Fix minor issues
Diffstat (limited to 'backends/lean/Base/Primitives')
0 files changed, 0 insertions, 0 deletions