Tealeaves.Backends.Adapters.NominaltoLN
From Tealeaves Require Import
Classes.Kleisli.DecoratedFunctorPoly
Backends.Nominal.Common.Binding
Backends.LN.LN.
Classes.Kleisli.DecoratedFunctorPoly
Backends.Nominal.Common.Binding
Backends.LN.LN.
Section with_DTM.
Context
{T: Type → Type → Type}.
Definition binding_to_ln: Binding → LN :=
fun b ⇒
match b with
| Bound prefix var postfix ⇒
Bd (length postfix)
| Unbound context var ⇒
Fr var
end.
Definition nomToLN_loc:
list name × name → LN.
Proof.
intros [ctx x].
exact (binding_to_ln (get_binding ctx x)).
Defined.
Definition nomToLN `{MapdPoly T}:
T name name → T unit LN :=
mapdp (T := T) (const tt) nomToLN_loc.
End with_DTM.
Context
{T: Type → Type → Type}.
Definition binding_to_ln: Binding → LN :=
fun b ⇒
match b with
| Bound prefix var postfix ⇒
Bd (length postfix)
| Unbound context var ⇒
Fr var
end.
Definition nomToLN_loc:
list name × name → LN.
Proof.
intros [ctx x].
exact (binding_to_ln (get_binding ctx x)).
Defined.
Definition nomToLN `{MapdPoly T}:
T name name → T unit LN :=
mapdp (T := T) (const tt) nomToLN_loc.
End with_DTM.