feature request: agda style term construction

cpitclaudel / company-coq

A Coq IDE build on top of Proof General's Coq mode

GNU General Public License v3.0

351 stars 29 forks source link

Open spitters opened 7 years ago

spitters commented 7 years ago

With 8.6 we seem to have most of the technology to create agda style term construction. agda manual

I thought I'd record it here.

@gares may also have insights into this.

cpitclaudel commented 7 years ago

Thanks! What's new in 8.6 that allows this?