Some renaming, for better display of docs/holes
commiteb99603f13fa778cb6cea58282c9377a7af717aa
authorEdwin Brady <ecb10@st-andrews.ac.uk>
dateSun 8 Nov 2015, 11:01 (11 years ago)
parent76b1675
libs/prelude/IO.idr+1−2
@@ -175,8 +175,7 @@ namespace FFI_C
175175 FFI_C : FFI
176176 FFI_C = MkFFI C_Types String String
177177
178−||| The type of interactive programs, performing some I/O side effects
179−||| and returning a value.
178+||| Interactive programs, describing I/O actions and returning a value.
180179||| @res The result type of the program
181180%error_reverse
182181IO : (res : Type) -> Type
libs/prelude/Prelude/Monad.idr+1−1
@@ -13,7 +13,7 @@ import IO
1313infixl 5 >>=
1414
1515class Applicative m => Monad (m : Type -> Type) where
16− (>>=) : m a -> (a -> m b) -> m b
16+ (>>=) : m a -> ((result : a) -> m b) -> m b
1717
1818||| Also called `join` or mu
1919flatten : Monad m => m (m a) -> m a
src/Idris/Core/TT.hs+1−1
@@ -1612,7 +1612,7 @@ pureTerm (Bind n b sc) = notClassName n && pureBinder b && pureTerm sc where
16121612 pureBinder (Let t v) = pureTerm t && pureTerm v
16131613 pureBinder t = pureTerm (binderTy t)
16141614
1615− notClassName (MN _ c) | c == txt "class" = False
1615+ notClassName (MN _ c) | c == txt "__class" = False
16161616 notClassName _ = True
16171617
16181618pureTerm _ = True
src/Idris/Elab/Class.hs+1−1
@@ -258,7 +258,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd
258258 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
259259 insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
260260 = PPi p n fc ty (insertConstraint c all sc)
261− insertConstraint c all sc = let dictN = sMN 0 "class"
261+ insertConstraint c all sc = let dictN = sMN 0 "__class"
262262 in PPi (constraint { pstatic = Static })
263263 dictN NoFC c
264264 (constrainMeths (map basename all)
src/Idris/Elab/Term.hs+1−1
@@ -363,7 +363,7 @@ elab ist info emode opts fn tm
363363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
364364 = do g <- goal; resolveTC' False False 5 g fn ist
365365 elab' ina fc (PResolveTC fc')
366− = do c <- getNameFrom (sMN 0 "class")
366+ = do c <- getNameFrom (sMN 0 "__class")
367367 instanceArg c
368368 -- Elaborate the equality type first homogeneously, then
369369 -- heterogeneously as a fallback