summaryrefslogtreecommitdiff
path: root/src/Helium/Algebra/Core.agda
diff options
context:
space:
mode:
authorGreg Brown <greg.brown@cl.cam.ac.uk>2022-01-07 09:59:41 +0000
committerGreg Brown <greg.brown@cl.cam.ac.uk>2022-01-07 09:59:41 +0000
commit568792d2890028fbf7d011393b6516af27cc8b2f (patch)
tree3a9f73f1990d127f85070ff0abde7812c135f016 /src/Helium/Algebra/Core.agda
parent5052a3f5ddf5cc65bb5a19e644b01694ba34d0f5 (diff)
Rename ⟦_⟧ to float.
Diffstat (limited to 'src/Helium/Algebra/Core.agda')
0 files changed, 0 insertions, 0 deletions