git.iko.soy/Idris-dev
on master help sign in
Some renaming, for better display of docs/holes
eb99603Edwin Brady
libs/prelude/IO.idr+1−2
compare with master
unifiedsplit
@@ -175,8 +175,7 @@ namespace FFI_C
175 FFI_C : FFI
175 FFI_C : FFI
176 FFI_C = MkFFI C_Types String String
176 FFI_C = MkFFI C_Types String String
177
177
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.
180||| @res The result type of the program
179||| @res The result type of the program
181%error_reverse
180%error_reverse
182IO : (res : Type) -> Type
181IO : (res : Type) -> Type
libs/prelude/Prelude/Monad.idr+1−1
@@ -13,7 +13,7 @@ import IO
13infixl 5 >>=
13infixl 5 >>=
14
14
15class Applicative m => Monad (m : Type -> Type) where
15class Applicative m => Monad (m : Type -> Type) where
16− (>>=) : m a -> (a -> m b) -> m b
16+ (>>=) : m a -> ((result : a) -> m b) -> m b
17
17
18||| Also called `join` or mu
18||| Also called `join` or mu
19flatten : Monad m => m (m a) -> m a
19flatten : 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
1612 pureBinder (Let t v) = pureTerm t && pureTerm v
1612 pureBinder (Let t v) = pureTerm t && pureTerm v
1613 pureBinder t = pureTerm (binderTy t)
1613 pureBinder t = pureTerm (binderTy t)
1614
1614
1615− notClassName (MN _ c) | c == txt "class" = False
1615+ notClassName (MN _ c) | c == txt "__class" = False
1616 notClassName _ = True
1616 notClassName _ = True
1617
1617
1618pureTerm _ = True
1618pureTerm _ = 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
258 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
258 insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm
259 insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
259 insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)
260 = PPi p n fc ty (insertConstraint c all sc)
260 = 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"
262 in PPi (constraint { pstatic = Static })
262 in PPi (constraint { pstatic = Static })
263 dictN NoFC c
263 dictN NoFC c
264 (constrainMeths (map basename all)
264 (constrainMeths (map basename all)
src/Idris/Elab/Term.hs+1−1
@@ -363,7 +363,7 @@ elab ist info emode opts fn tm
363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
363 elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes
364 = do g <- goal; resolveTC' False False 5 g fn ist
364 = do g <- goal; resolveTC' False False 5 g fn ist
365 elab' ina fc (PResolveTC fc')
365 elab' ina fc (PResolveTC fc')
366− = do c <- getNameFrom (sMN 0 "class")
366+ = do c <- getNameFrom (sMN 0 "__class")
367 instanceArg c
367 instanceArg c
368 -- Elaborate the equality type first homogeneously, then
368 -- Elaborate the equality type first homogeneously, then
369 -- heterogeneously as a fallback
369 -- heterogeneously as a fallback