Closed heueristik closed 1 month ago
Currently, one needs to use Set.fromList [member] to create a set with a single member.
Set.fromList [member]
Add another constructor, allowing to create sets with a single member.
singleton {A} {{Ord A}} (a : A) : Set A := Set.insert a Set.empty;
Do the same for Map as well
Map
Currently, one needs to use
Set.fromList [member]
to create a set with a single member.Add another constructor, allowing to create sets with a single member.
Do the same for
Map
as well