Documentation for provided postulates

src/Idris/Elab/Provider.hs

@@ -98,11 +98,7 @@ elabProvider doc info syn fc what n
                   logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
              | ProvPostulate _ <- what ->
                do -- Add the postulate
-                  elabPostulate
-                    info syn
-                    (fmap (const (Left $ Msg "")) .
-                     parseDocstring $ T.pack "Provided postulate")
-                    fc [] n (delab i tm)
+                  elabPostulate info syn doc fc [] n (delab i tm)
                   logLvl 3 $ "Elaborated provided postulate " ++ show n
              | otherwise ->
                ierror . Msg $ "Attempted to provide a postulate where a term was expected."

test/docs002/docs002.idr

@@ -12,5 +12,9 @@ getType _ = return (Provide Bool)
 
 ||| Some documentation
 %provide (T1 : Type) with getType 0
+
 ||| Some other documentation
 %provide (T2 : Type) with getType 1
+
+||| Some provided postulate
+%provide postulate T3 with getType 0

test/docs002/expected

@@ -5,4 +5,7 @@ Type checking ./docs002.idr
 *docs002> T2 : Type
     Some other documentation
     
+*docs002> T3 : Int
+    Some provided postulate
+    
 *docs002> Bye bye

test/docs002/input

@@ -1,2 +1,3 @@
 :doc T1
 :doc T2
+:doc T3