xplat

= 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.

xplat

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) ()