|
|
f5457d8841
|
Move proof of least element into FiniteHeightLattice
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-07-26 13:16:22 +02:00 |
|
|
|
b0488c9cc6
|
Make 'IsDecidable' into a record to aid instance search
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2025-01-04 18:58:56 -08:00 |
|
|
|
828b652d3b
|
Rename 'a' to 'b' in fixedpoint algorithm proof
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-08-18 10:28:45 -10:00 |
|
|
|
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 |
|
|
|
512cd22be5
|
Fix definition of 'less than' to not involve a third variable.
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2024-02-07 21:04:13 -08:00 |
|
|
|
9646096c75
|
Fix uses of 'absurd' in Fixedpoint.agda
|
2023-11-23 14:15:40 -08:00 |
|
|
|
e4f87175a0
|
Remove IsDecidable record in favor of a plain definition
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-09-17 19:43:24 -07:00 |
|
|
|
e3b8cc39f1
|
Put the fixed point algorithm code into its own file
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
|
2023-09-16 13:39:35 -07:00 |
|
