16 Commits

Author	SHA1	Message	Date
Danila Fedorin	311ed75186	Expose more helpers from 'Map' ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-03-09 13:57:02 -08:00
Danila Fedorin	7905d106e2	Tweak signature of 'forget' to simplify proofs ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-03-07 20:04:33 -08:00
Danila Fedorin	34203840c8	Use the new provenance function to clean up some proofs ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-03-07 19:59:14 -08:00
Danila Fedorin	48983c55b1	Prove exercise 4.26 from the textbook ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-03-06 00:35:29 -08:00
Danila Fedorin	0774946211	Expose decidability from Map modules ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-03-01 23:27:49 -08:00
Danila Fedorin	8715d6d89c	Finish proof of from distributivity ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-26 00:00:18 -08:00
Danila Fedorin	d6064ff752	Expose 'locate' and 'forget' from Map ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-25 18:07:50 -08:00
Danila Fedorin	99fc21cef2	Expose 'subset-impl' from Map ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-25 13:57:28 -08:00
Danila Fedorin	e89418d600	Expose bundle form 'Map' ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-11 21:12:49 -08:00
Danila Fedorin	ec31333e9a	Add a 'Finite Map' lattice ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-11 14:19:41 -08:00
Danila Fedorin	ad26d20274	Add facts about equal-key maps ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-11 12:45:43 -08:00
Danila Fedorin	d718338759	Clean up 'Map' to hide implementation details, extract code ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-10 16:51:43 -08:00
Danila Fedorin	1b8c88b1a2	Expose only a 'public' "keys" function from Map ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2024-02-10 16:35:21 -08:00
Danila Fedorin	3c346dcd15	Add a 'set' lattice backed by maps ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-09-23 17:12:12 -07:00
Danila Fedorin	5d54e62c3a	Move the lattice etc. instances into Lattice.Map ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-09-23 15:08:04 -07:00
Danila Fedorin	845a8a2236	Move the Map into Lattice/Map ... Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>	2023-09-23 15:06:43 -07:00