cornelis icon indicating copy to clipboard operation
cornelis copied to clipboard

Published 20 hours ago • verified publisher icon isovector

Cmd_give after refinement / etc

Open isovector opened this issue 2 years ago • 0 comments

Cmd_give lets agda update its internal state without requiring a subsequent reload. emacs asks for a refinement and then immediately gives it back. Cornelis should do the same.

Can we ignore the range option? that'd be greaaaat

isovector avatar Jun 16 '22 15:06 isovector