World names

Closes #7
This commit is contained in:
Alexander Bentkamp
2023-01-20 11:36:44 +01:00
parent 6e0469d3bf
commit 719b8d2964
4 changed files with 14 additions and 8 deletions
@@ -114,9 +114,9 @@ structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
edges: Array (α × α) := {}
deriving Inhabited
instance [inst : BEq α] [inst : Hashable α] [ToJson α] [ToJson β] : ToJson (Graph α β) := {
instance [ToJson β] : ToJson (Graph Name β) := {
toJson := fun graph => Json.mkObj [
("nodes", toJson (graph.nodes.toArray.map Prod.snd)),
("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
("edges", toJson graph.edges)
]
}