diff --git a/src/Idris/Help.hs b/src/Idris/Help.hs index 842f6f0ee..6b379ec65 100644 --- a/src/Idris/Help.hs +++ b/src/Idris/Help.hs @@ -91,4 +91,6 @@ extraHelp = , ([":proofsearch!", ":ps!"], NoArg, ":ps! destructively does proof search for name on line, with names as hints") , ([":addproofclause", ":apc"], NoArg, ":apc adds a pattern-matching proof clause to name on line") , ([":addproofclause!", ":apc!"], NoArg, ":apc! destructively adds a pattern-matching proof clause to name on line") + , ([":refine", ":ref"], NoArg, ":ref attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable") + , ([":refine!", ":ref!"], NoArg, ":ref! destructively attempts to partially solve name on line, with name' as hint, introducing metavariables for arguments that aren't inferrable") ]