Enable type inference for Menhir.

RedPRL / redtt

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Apache License 2.0

204 stars 12 forks source link

Closed fpottier closed 2 years ago

fpottier commented 2 years ago

This is already useful now, and will be more useful in the future (Menhir's upcoming new code back-end will require --infer).

favonia commented 2 years ago

(Hmm Travis is no longer working, it seems.)