Very basic example of using elaborator reflection to interactively fill in a hole in a function implementation.

SimpleElaborationExample.idr

-- Note that :elab does not automatically do :module Language.Reflection.Elab
-- for you. When you finish a proof, the same applies, so we have to also
-- add an import statement here, otherwise we'll get an error:
--
--     When checking right hand side of Main.shouldBeEmptyString:
--     No such variable Language.Reflection.Elab.Elab
import Language.Reflection.Elab

fillMeIn : List String -> String
fillMeIn strings =
    case strings of
        Nil =>
            -- The ? creates a hole. This can be interactively filled using
            -- :elab at the Idris REPL. On completion of the proof,
            -- it writes out a definition that you can paste into the file.
            ?shouldBeEmptyString

        string :: _ =>
            string


-- This is the definition written out on :qed.
-- Try commenting this out and using :elab to fill the hole yourself.
-- Don't forget to run :module Language.Reflection.Elab first!
--
-- Once you have that working, try replacing the strings variable with an
-- unused variable (hint: look at `:doc intro`, then `:doc TTName`).
{-
Main.shouldBeEmptyString = %runElab (do intro $ UN "strings"
                                        fill $ RConstant $ Str ""
                                        solve)
-}

{-
*SimpleElaborationExample> :printdef fillMeIn
fillMeIn : List String -> String
fillMeIn strings = case strings of
                     [] => shouldBeEmptyString strings
                     (string :: _) => string



*SimpleElaborationExample> :printdef shouldBeEmptyString
shouldBeEmptyString : List String -> String
shouldBeEmptyString = let tacticExpr =
                            PE_>>=_585bb10e (intro (UN "strings"))
                                            (\bindx =>
                                               PE_>>=_585bb10e (fill (RConstant (Str "")))
                                                               (\bindx =>
                                                                  solve))
                      in \strings => ""


*SimpleElaborationExample> fillMeIn []
"" : String
*SimpleElaborationExample> fillMeIn ["hi", "there"]
"hi" : String
-}