 Danila Fedorin
|
16fa4cd1d8
|
Use records rather than nested pairs to represent 'fixed height'
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-05-09 20:11:04 -07:00 |
|
Danila Fedorin
|
2ddac38c3f
|
Update with new changes to Agda
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-03 16:44:10 -08:00 |
|
Danila Fedorin
|
97a4165b58
|
Expose bundles from FiniteValueMap
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-03-01 21:35:40 -08:00 |
|
Danila Fedorin
|
d280f5afdf
|
Make auxillary definitions private
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-25 14:06:45 -08:00 |
|
Danila Fedorin
|
aafcb2683d
|
Prove the transport of 'height lattice' property given an isomorphism
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-18 23:26:41 -08:00 |