git.iko.soy/Idris-dev
on master help sign in
Documentation for provided postulates
commit54fb787ac1c096a035461acf9c5e2ef98e7f7146 authorAdam Sandberg Eriksson <adam@sandbergericsson.se> dateSun 15 Mar 2015, 15:16 (12 years ago) parentad2f186
4 files changed+9−5
compare with master
unifiedsplit
src/Idris/Elab/Provider.hs+1−5 test/docs002/docs002.idr+4 test/docs002/expected+3 test/docs002/input+1
src/Idris/Elab/Provider.hs+1−5
@@ -98,11 +98,7 @@ elabProvider doc info syn fc what n
9898 logLvl 3 $ "Elaborated provider " ++ show n ++ " as: " ++ show tm
9999 | ProvPostulate _ <- what ->
100100 do -- Add the postulate
101− elabPostulate
102− info syn
103− (fmap (const (Left $ Msg "")) .
104− parseDocstring $ T.pack "Provided postulate")
105− fc [] n (delab i tm)
101+ elabPostulate info syn doc fc [] n (delab i tm)
106102 logLvl 3 $ "Elaborated provided postulate " ++ show n
107103 | otherwise ->
108104 ierror . Msg $ "Attempted to provide a postulate where a term was expected."
test/docs002/docs002.idr+4
@@ -12,5 +12,9 @@ getType _ = return (Provide Bool)
1212
1313||| Some documentation
1414%provide (T1 : Type) with getType 0
15+
1516||| Some other documentation
1617%provide (T2 : Type) with getType 1
18+
19+||| Some provided postulate
20+%provide postulate T3 with getType 0
test/docs002/expected+3
@@ -5,4 +5,7 @@ Type checking ./docs002.idr
55*docs002> T2 : Type
66 Some other documentation
77
8+*docs002> T3 : Int
9+ Some provided postulate
10+
811*docs002> Bye bye
test/docs002/input+1
@@ -1,2 +1,3 @@
11:doc T1
22:doc T2
3+:doc T3