Commit e1360eba authored by POTTIER Francois's avatar POTTIER Francois

TODO.

parent f53a41e7
...@@ -5,14 +5,14 @@ TODO (REALLY): ...@@ -5,14 +5,14 @@ TODO (REALLY):
Relax ba so as to not require well-formedness? Relax ba so as to not require well-formedness?
Define wf separately, relying on ba_wf internally. Define wf separately, relying on ba_wf internally.
Global uniqueness, or uniqueness along a branch? Global uniqueness, or uniqueness along a branch?
Which wf criterion do we want? Which wf criterion do we want? both?
Implement avoid, which renames the bound names of a term so as to Implement avoid, which renames the bound names of a term so as to
avoid a certain set of names. avoid a certain set of names.
Implement fused copy/subst, fused avoid/subst? Implement fused copy/subst, fused avoid/subst?
Implement a kit that composes two kits, so as to easily Implement a kit that composes two kits, so as to easily implement fused operations.
implement fused operations. Composition of classes? Or composition of kit objects? ...
Suppose I want to annotate every abstraction with its fa. Suppose I want to annotate every abstraction with its fa.
Or, suppose I want to annotate every abstraction with the Or, suppose I want to annotate every abstraction with the
......
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