diff options
| author | Andreas Grois <andi@grois.info> | 2024-12-01 19:58:11 +0100 |
|---|---|---|
| committer | Andreas Grois <andi@grois.info> | 2024-12-01 19:58:11 +0100 |
| commit | 4784df61d4858f9f470327e46822aabf2f7eff52 (patch) | |
| tree | d043f34de8e0dacebf6ca3b66ec8b66fbee5f8f6 /Common/Helpers.lean | |
| parent | 11639a915b229952c267deb03a367ef70bb4a27e (diff) | |
Minor, indentation
Diffstat (limited to 'Common/Helpers.lean')
0 files changed, 0 insertions, 0 deletions