Commit 5f8cdc5f authored by Ralf Jung's avatar Ralf Jung

annotate where we have binders

parent de973b37
......@@ -57,7 +57,7 @@ Instance Rename_expr : Rename expr. derive. Defined.
Instance Subst_expr : Subst expr. derive. Defined.
Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
Definition Lam (e: expr) := Rec (e.[up ids]).
Definition Lam (e: {bind expr}) := Rec (e.[up ids]).
Definition LitUnit := Lit tt.
Definition LitTrue := Lit true.
Definition LitFalse := Lit false.
......
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