git.iko.soy/Idris-dev
on master help sign in
Fix typo in effects tutorial
d3fa352Edwin Brady
docs/effects/introduction.rst+1−1
compare with master
unifiedsplit
@@ -53,7 +53,7 @@ this specific example later.
53Hello world
53Hello world
54===========
54===========
55
55
56−To give an idea of how programs with effects look in , here is the
56+To give an idea of how programs with effects look, here is the
57ubiquitous “Hello world” program, written using the ``Effects``
57ubiquitous “Hello world” program, written using the ``Effects``
58library:
58library:
59
59
src/Idris/Delaborate.hs+10−10
@@ -147,22 +147,22 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
147 = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)
147 = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)
148 de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)
148 de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)
149 | toplevel_imp impl -- information in 'imps' repeated
149 | toplevel_imp impl -- information in 'imps' repeated
150− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC
150+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC
151 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
151 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
152 de tys env is (Bind n (Pi rig (Just impl) ty _) sc)
152 de tys env is (Bind n (Pi rig (Just impl) ty _) sc)
153 | tcimplementation impl
153 | tcimplementation impl
154− = PPi constraint n NoFC (de tys env [] ty)
154+ = PPi constraint n NoFC (de tys env [] ty)
155 (de ((n, ty) : tys) ((n,n):env) is sc)
155 (de ((n, ty) : tys) ((n,n):env) is sc)
156 | otherwise
156 | otherwise
157 = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)
157 = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)
158 de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)
158 de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)
159− = PPi (Imp opts Dynamic False Nothing False rig) n NoFC
159+ = PPi (Imp opts Dynamic False Nothing False rig) n NoFC
160 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
160 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
161 de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)
161 de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)
162− = PPi (constraint { pcount = rig}) n NoFC
162+ = PPi (constraint { pcount = rig}) n NoFC
163 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
163 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
164 de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)
164 de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)
165− = PPi ((tacimpl tac) { pcount = rig }) n NoFC
165+ = PPi ((tacimpl tac) { pcount = rig }) n NoFC
166 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
166 (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)
167 de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)
167 de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)
168 = PPi (Exp (argopts plic) Dynamic False rig)
168 = PPi (Exp (argopts plic) Dynamic False rig)
@@ -170,7 +170,7 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
170 (de tys env [] ty)
170 (de tys env [] ty)
171 (de ((n, ty) : tys) ((n,n):env) is sc)
171 (de ((n, ty) : tys) ((n,n):env) is sc)
172 de tys env [] (Bind n (Pi rig _ ty _) sc)
172 de tys env [] (Bind n (Pi rig _ ty _) sc)
173− = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)
173+ = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)
174 (de ((n, ty) : tys) ((n,n):env) [] sc)
174 (de ((n, ty) : tys) ((n,n):env) [] sc)
175
175
176 de tys env imps (Bind n (Let ty val) sc)
176 de tys env imps (Bind n (Let ty val) sc)
@@ -179,7 +179,7 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
179 , (P _ cOp _, args) <- unApply sc
179 , (P _ cOp _, args) <- unApply sc
180 , Just caseblock <- delabCase tys env imps val cOp args = caseblock
180 , Just caseblock <- delabCase tys env imps val cOp args = caseblock
181 | otherwise =
181 | otherwise =
182− PLet un n NoFC (de tys env [] ty)
182+ PLet un n NoFC (de tys env [] ty)
183 (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)
183 (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)
184 de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
184 de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
185 de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
185 de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc
@@ -235,10 +235,10 @@ delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm
235 | Just imps <- lookupCtxtExact n (idris_implicits ist)
235 | Just imps <- lookupCtxtExact n (idris_implicits ist)
236 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
236 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)
237 | otherwise = PApp un (PRef un [] n) (map pexp args)
237 | otherwise = PApp un (PRef un [] n) (map pexp args)
238− where
238+ where
239− findImp (Bind n (Pi _ im@(Just i) _ _) sc)
239+ findImp (Bind n (Pi _ im@(Just i) _ _) sc)
240 = pimp n Placeholder True : findImp sc
240 = pimp n Placeholder True : findImp sc
241− findImp (Bind n (Pi _ _ _ _) sc)
241+ findImp (Bind n (Pi _ _ _ _) sc)
242 = pexp Placeholder : findImp sc
242 = pexp Placeholder : findImp sc
243 findImp _ = []
243 findImp _ = []
244 imp (PImp p m l n _) arg = PImp p m l n arg
244 imp (PImp p m l n _) arg = PImp p m l n arg
src/Idris/Elab/Utils.hs+1−1
@@ -211,7 +211,7 @@ psolve tm = return ()
211
211
212pvars ist tm = pv' [] tm
212pvars ist tm = pv' [] tm
213 where
213 where
214− pv' env (Bind n (PVar _ t) sc)
214+ pv' env (Bind n (PVar _ t) sc)
215 = (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc
215 = (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc
216 pv' env _ = []
216 pv' env _ = []
217
217