Idris2 icon indicating copy to clipboard operation
Idris2 copied to clipboard

Published 20 hours ago • verified publisher icon idris-lang

Add fromTTImp, fromName, and fromDecls

Open madman-bob opened this issue 8 months ago • 0 comments

This follows on from #2930. Now that we've had a version bump, we can bind fromTTImp, fromName, and fromDecls in base.

madman-bob avatar Jun 17 '24 14:06 madman-bob