Skip to content

Instantly share code, notes, and snippets.

newtype WrappedShow1 f a = WrappedShow1 (f a)
instance (Show1 f, Show a) => Show (WrappedShow1 f a) where
showsPrec x = liftShowsPrec showsPrec showList
showList x = liftShowList showsPrec showList
-- instance Show1 YourThing where
-- liftShowsPrec = reifyShow (const showsPrec) ()
-- liftShowList = reifyShow (const showList) ()
@xplat
xplat / agda-wishlist.txt
Created May 18, 2011 20:51
agda wishlist
= agda-mode
* C-c C-c should accept an expression and create a with. (does it do this already?) Or there should be another key combo to create a with.
* C-c C-c should work from inside complex expressions, not just when the RHS is a single hole. Variables know where they are bound, and the RHS can be duplicated and specialized.
* A key combo to rename a variable in scope. [should this include occurrences outside the current module? in general that would require an IDE-style project system ...]
* Undo without reload.
* Preview for agsy and null refine. [maybe redundant with the above]
* A key combo to suck the region into a hole.
* A key combo to expand a hole to the next higher node in the syntax tree.
! More consistent yellow highlighting during smart editing without reload.