|
|
@ -14,17 +14,26 @@ Module dbterm.
|
|
|
|
.
|
|
|
|
.
|
|
|
|
|
|
|
|
|
|
|
|
(** Formalize substitutions and renamings as functions. *)
|
|
|
|
(** Formalize substitutions and renamings as functions. *)
|
|
|
|
Definition subt := nat → expr.
|
|
|
|
Definition sub_t := nat → expr.
|
|
|
|
Definition rent := nat → nat.
|
|
|
|
Definition ren_t := nat → nat.
|
|
|
|
|
|
|
|
|
|
|
|
Implicit Types
|
|
|
|
Implicit Types
|
|
|
|
(σ : subt)
|
|
|
|
(σ : sub_t)
|
|
|
|
(δ : rent)
|
|
|
|
(δ : ren_t)
|
|
|
|
(n x : nat)
|
|
|
|
(n x : nat)
|
|
|
|
(e : expr).
|
|
|
|
(e : expr).
|
|
|
|
|
|
|
|
|
|
|
|
Fixpoint subst σ e :=
|
|
|
|
Fixpoint subst σ e :=
|
|
|
|
(* FIXME *) e.
|
|
|
|
match e with
|
|
|
|
|
|
|
|
| Lit l => Lit l
|
|
|
|
|
|
|
|
| Var i => σ i
|
|
|
|
|
|
|
|
| Lam e => Lam (subst (λ n, match n with
|
|
|
|
|
|
|
|
| 0 => Var 0
|
|
|
|
|
|
|
|
| S n => σ n
|
|
|
|
|
|
|
|
))
|
|
|
|
|
|
|
|
| Plus e1 e2 => Plus (subst σ a) (subst σ b)
|
|
|
|
|
|
|
|
| App e_fn e_arg =>
|
|
|
|
|
|
|
|
end.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|