Commit 6c427c8a authored by Raphaël Cauderlier's avatar Raphaël Cauderlier
Browse files

Conversion from records to association lists

parent 795d3bd4
......@@ -197,3 +197,19 @@ AssocT_list_record : f : Typer ->
L : AssocT_list f ->
Record f (AssocT_list_domain f L)
:= assocT_val.
(; To association lists ;)
to_assoc_list : f : Typer ->
D : Domain ->
Record f D ->
Assoc_list
:=
f : Typer =>
D : Domain =>
R : Record f D =>
dk_list.map
label
triple
(l : Label => mk_triple l (f l) (R l))
D.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment