Closed Halbaroth closed 4 months ago
The smart constructor mk_binders is useless because we can build directly the set of binders in D_cnf and we avoid to embed variables in symbols then extract them in mk_binders.
mk_binders
D_cnf
The smart constructor
mk_bindersis useless because we can build directly the set of binders inD_cnfand we avoid to embed variables in symbols then extract them inmk_binders.