summaryrefslogtreecommitdiff
path: root/backends/lean
diff options
context:
space:
mode:
authorAymeric Fromherz2024-05-24 12:47:43 +0200
committerAymeric Fromherz2024-05-24 12:47:43 +0200
commit50dbeaeb018ab2cb44df3f557f1958eb15351f31 (patch)
tree51c73a3b0ddbf790f1f93892c67ccb2fb55d4f58 /backends/lean
parente669de58b71fd68642cfacf1a2e3cbd1c5b2f4fe (diff)
Rename span into raw_span
Diffstat (limited to '')
0 files changed, 0 insertions, 0 deletions