summaryrefslogtreecommitdiff
path: root/Common/Option.lean
diff options
context:
space:
mode:
authorAndreas Grois <andi@grois.info>2023-12-18 20:42:08 +0100
committerAndreas Grois <andi@grois.info>2023-12-18 20:42:08 +0100
commit214f0bdcbe35a9b6e68ae0b78a502fa2faaca5d6 (patch)
treef3d00021dc6830ec572c8851b9db4271018c2fa2 /Common/Option.lean
parent0f942c82d9b1cb74aad2dd667c2d53f63a38d7a2 (diff)
Partial cleanup of Heap
Diffstat (limited to 'Common/Option.lean')
0 files changed, 0 insertions, 0 deletions