Skip to content

Draft: experiment: use coq's ability to infer more canonical structures

Ralf Jung requested to merge ralf/ra-infer into master

I wonder if we should recommend this style, once all Coq versions we support can handle it. It is certainly much nicer, we could entirely hide these R/UR terms from users. Unfortunately in one case already in this repo, it requires more type annotations. I don't understand why Coq cannot infer that any more.

Edited by Ralf Jung

Merge request reports