issues
search
Deducteam
/
lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Other
269
stars
35
forks
source link
improve export to Coq
#976
Closed
fblanqui
closed
1 year ago
fblanqui
commented
1 year ago
add 2 new options for export command:
--erasing
and
--requiring
improve handling of builtins
improve Coq output readability
--erasingand--requiring