search

Deducteam / lambdapi

Proof assistant based on the λΠ-calculus modulo rewriting
Other
265 stars 35 forks source link

coq export: do not fail, only warn when a command is not translated #1091

Closed fblanqui closed 2 months ago

fblanqui commented 2 months ago

and update doc: with -o stt_coq, parameters with no type are assumed to be of type Set