diff --git a/CONTRIBUTORS b/CONTRIBUTORS
index ec57c58010..84c0e5533f 100644
--- a/CONTRIBUTORS
+++ b/CONTRIBUTORS
@@ -3,10 +3,12 @@ Thanks to the following for their help and contributions:
 Ozgur Akgun
 Nicola Botta
 Edwin Brady
+David Raymond Christiansen
 Jason Dagit
 Cezar Ionescu
 Irene Knapp
 Mathnerd314
+Hannes Mehnert
 Mekeor Melire
 Melissa Mozifian
 Dominic Mulligan
@@ -20,4 +22,3 @@ Dirk Ullrich
 Leif Warner
 Daniel Waterworth
 Jonas Westerlund
-David Raymond Christiansen
diff --git a/idris.cabal b/idris.cabal
index 0a1920e98b..cac13f9570 100644
--- a/idris.cabal
+++ b/idris.cabal
@@ -77,7 +77,7 @@ Executable     idris
                               Core.CaseTree, Core.Constraints,
 
                               Idris.AbsSyntax, Idris.AbsSyntaxTree,
-                              Idris.Parser, Idris.REPL,
+                              Idris.Parser, Idris.Help, Idris.REPL,
                               Idris.REPLParser, Idris.ElabDecls, Idris.Error,
                               Idris.Delaborate, Idris.Primitives, Idris.Imports,
                               Idris.Compiler, Idris.Prover, Idris.ElabTerm,
diff --git a/src/Idris/Completion.hs b/src/Idris/Completion.hs
index e993cad953..3d68ca7eae 100644
--- a/src/Idris/Completion.hs
+++ b/src/Idris/Completion.hs
@@ -6,6 +6,7 @@ import Core.TT
 import Core.CoreParser (opChars)
 
 import Idris.AbsSyntaxTree
+import Idris.Help
 
 import Control.Monad.State.Strict
 
@@ -14,40 +15,11 @@ import Data.Maybe
 
 import System.Console.Haskeline
 
--- TODO: add specific classes of identifiers to complete, fx metavariables
--- | A specification of the arguments that REPL commands can take
-data CmdArg = ExprArg -- ^ The command takes an expression
-            | NameArg -- ^ The command takes a name
-            | FileArg -- ^ The command takes a file
-            | ModuleArg -- ^ The command takes a module name
-            | OptionArg -- ^ The command takes an option
-            | MetaVarArg -- ^ The command takes a metavariable
-
--- | Information about how to complete the various commands
-cmdArgs :: [(String, CmdArg)]
-cmdArgs = [ (":t", ExprArg)
-          , (":miss", NameArg)
-          , (":missing", NameArg)
-          , (":i", NameArg)
-          , (":info", NameArg)
-          , (":total", NameArg)
-          , (":l", FileArg)
-          , (":load", FileArg)
-          , (":m", ModuleArg) -- NOTE: Argumentless form is a different command
-          , (":p", MetaVarArg)
-          , (":prove", MetaVarArg)
-          , (":a", NameArg)
-          , (":addproof", NameArg)
-          , (":rmproof", NameArg)
-          , (":showproof", NameArg)
-          , (":c", FileArg)
-          , (":compile", FileArg)
-          , (":js", FileArg)
-          , (":javascript", FileArg)
-          , (":set", OptionArg)
-          , (":unset", OptionArg)
-          ]
-commands = map fst cmdArgs
+
+fst4 :: (a, b, c, d) -> a
+fst4 (a, b, c, d) = a
+
+commands = concatMap fst4 help
 
 -- | A specification of the arguments that tactics can take
 data TacticArg = NameTArg -- ^ Names: n1, n2, n3, ... n
@@ -124,15 +96,22 @@ completeOption = completeWord Nothing " \t" completeOpt
 isWhitespace :: Char -> Bool
 isWhitespace = (flip elem) " \t\n"
 
+lookupInHelp :: String -> Maybe CmdArg
+lookupInHelp cmd = lookupInHelp' cmd help
+    where lookupInHelp' cmd ((cmds, _, _, arg):xs) | elem cmd cmds = Just arg
+                                                   | otherwise   = lookupInHelp' cmd xs
+          lookupInHelp' cmd [] = Nothing
+
 -- | Get the completion function for a particular command
 completeCmd :: String -> CompletionFunc Idris
-completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookup cmd cmdArgs
+completeCmd cmd (prev, next) = fromMaybe completeCmdName $ fmap completeArg $ lookupInHelp cmd
     where completeArg FileArg = completeFilename (prev, next)
           completeArg NameArg = completeExpr [] (prev, next) -- FIXME only complete one name
           completeArg OptionArg = completeOption (prev, next)
           completeArg ModuleArg = noCompletion (prev, next) -- FIXME do later
           completeArg ExprArg = completeExpr [] (prev, next)
           completeArg MetaVarArg = completeMetaVar (prev, next) -- FIXME only complete one name
+          completeArg NoArg = noCompletion (prev, next)
           completeCmdName = return $ ("", completeWith commands cmd)
 
 -- | Complete REPL commands and defined identifiers
diff --git a/src/Idris/Help.hs b/src/Idris/Help.hs
new file mode 100644
index 0000000000..d892a2cb95
--- /dev/null
+++ b/src/Idris/Help.hs
@@ -0,0 +1,36 @@
+module Idris.Help (CmdArg(..), help) where
+
+data CmdArg = ExprArg -- ^ The command takes an expression
+            | NameArg -- ^ The command takes a name
+            | FileArg -- ^ The command takes a file
+            | ModuleArg -- ^ The command takes a module name
+            | OptionArg -- ^ The command takes an option
+            | MetaVarArg -- ^ The command takes a metavariable
+            | NoArg -- ^ No completion yet
+
+
+help :: [([String], String, String, CmdArg)]
+help =
+  [ (["<expr>"], "", "Evaluate an expression", NoArg),
+    ([":t"], "<expr>", "Check the type of an expression", ExprArg),
+    ([":miss", ":missing"], "<name>", "Show missing clauses", NameArg),
+    ([":i", ":info"], "<name>", "Display information about a type class", NameArg),
+    ([":total"], "<name>", "Check the totality of a name", NameArg),
+    ([":r",":reload"], "", "Reload current file", NoArg),
+    ([":l",":load"], "<filename>", "Load a new file", FileArg),
+    ([":m",":module"], "<module>", "Import an extra module", ModuleArg), -- NOTE: dragons
+    ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL", NoArg),
+    ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)", MetaVarArg),
+    ([":p",":prove"], "<name>", "Prove a metavariable", MetaVarArg),
+    ([":a",":addproof"], "<name>", "Add proof to source file", NameArg),
+    ([":rmproof"], "<name>", "Remove proof from proof stack", NameArg),
+    ([":showproof"], "<name>", "Show proof", NameArg),
+    ([":proofs"], "", "Show available proofs", NoArg),
+    ([":c",":compile"], "<filename>", "Compile to an executable <filename>", FileArg),
+    ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>", FileArg),
+    ([":exec",":execute"], "", "Compile to an executable and run", NoArg),
+    ([":?",":h",":help"], "", "Display this help text", NoArg),
+    ([":set"], "<option>", "Set an option (errorcontext, showimplicits)", OptionArg),
+    ([":unset"], "<option>", "Unset an option", OptionArg),
+    ([":q",":quit"], "", "Exit the Idris system", NoArg)
+  ]
diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs
index 2270b1db7f..5475b433a5 100644
--- a/src/Idris/REPL.hs
+++ b/src/Idris/REPL.hs
@@ -16,6 +16,7 @@ import Idris.Primitives
 import Idris.Coverage
 import Idris.UnusedArgs
 import Idris.Docs
+import Idris.Help
 import Idris.Completion
 
 import Paths_idris
@@ -418,8 +419,9 @@ showTotalN i n = case lookupTotal n (tt_ctxt i) of
 displayHelp = let vstr = showVersion version in
               "\nIdris version " ++ vstr ++ "\n" ++
               "--------------" ++ map (\x -> '-') vstr ++ "\n\n" ++
+              concatMap cmdInfo helphead ++
               concatMap cmdInfo help
-  where cmdInfo (cmds, args, text) = "   " ++ col 16 12 (showSep " " cmds) args text 
+  where cmdInfo (cmds, args, text, _) = "   " ++ col 16 12 (showSep " " cmds) args text 
         col c1 c2 l m r = 
             l ++ take (c1 - length l) (repeat ' ') ++ 
             m ++ take (c2 - length m) (repeat ' ') ++ r ++ "\n"
@@ -469,31 +471,9 @@ parseArgs ("--dumpcases":n:ns)  = DumpCases n : (parseArgs ns)
 parseArgs ("--target":n:ns)     = UseTarget (parseTarget n) : (parseArgs ns)
 parseArgs (n:ns)                = Filename n : (parseArgs ns)
 
-help =
-  [ (["Command"], "Arguments", "Purpose"),
-    ([""], "", ""),
-    (["<expr>"], "", "Evaluate an expression"),
-    ([":t"], "<expr>", "Check the type of an expression"),
-    ([":miss", ":missing"], "<name>", "Show missing clauses"),
-    ([":i", ":info"], "<name>", "Display information about a type class"),
-    ([":total"], "<name>", "Check the totality of a name"),
-    ([":r",":reload"], "", "Reload current file"),
-    ([":l",":load"], "<filename>", "Load a new file"),
-    ([":m",":module"], "<module>", "Import an extra module"),
-    ([":e",":edit"], "", "Edit current file using $EDITOR or $VISUAL"),
-    ([":m",":metavars"], "", "Show remaining proof obligations (metavariables)"),
-    ([":p",":prove"], "<name>", "Prove a metavariable"),
-    ([":a",":addproof"], "<name>", "Add proof to source file"),
-    ([":rmproof"], "<name>", "Remove proof from proof stack"),
-    ([":showproof"], "<name>", "Show proof"),
-    ([":proofs"], "", "Show available proofs"),
-    ([":c",":compile"], "<filename>", "Compile to an executable <filename>"),
-    ([":js", ":javascript"], "<filename>", "Compile to JavaScript <filename>"),
-    ([":exec",":execute"], "", "Compile to an executable and run"),
-    ([":?",":h",":help"], "", "Display this help text"),
-    ([":set"], "<option>", "Set an option (errorcontext, showimplicits)"),
-    ([":unset"], "<option>", "Unset an option"),
-    ([":q",":quit"], "", "Exit the Idris system")
+helphead =
+  [ (["Command"], "Arguments", "Purpose", ""),
+    ([""], "", "", "")
   ]