diff --git a/libs/base/Data/IORef.idr b/libs/base/Data/IORef.idr index ebdf37851..347929066 100644 --- a/libs/base/Data/IORef.idr +++ b/libs/base/Data/IORef.idr @@ -18,10 +18,12 @@ newIORef val = do m <- primIO (prim__newIORef val) pure (MkRef m) +%inline export readIORef : IORef a -> IO a readIORef (MkRef m) = primIO (prim__readIORef m) +%inline export writeIORef : IORef a -> (1 val : a) -> IO () writeIORef (MkRef m) val = primIO (prim__writeIORef m val) diff --git a/libs/prelude/Prelude.idr b/libs/prelude/Prelude.idr index 69968a75f..7a6cadb4b 100644 --- a/libs/prelude/Prelude.idr +++ b/libs/prelude/Prelude.idr @@ -373,6 +373,7 @@ interface Num ty => Integral ty where -- Integer +%inline public export Num Integer where (+) = prim__add_Integer @@ -408,6 +409,7 @@ defaultInteger = %search -- Int +%inline public export Num Int where (+) = prim__add_Int @@ -914,11 +916,13 @@ public export Right x == Right x' = x == x' _ == _ = False +%inline public export Functor (Either e) where map f (Left x) = Left x map f (Right x) = Right (f x) +%inline public export Applicative (Either e) where pure = Right diff --git a/src/Idris/Desugar.idr b/src/Idris/Desugar.idr index c54ae1f77..8578a6346 100644 --- a/src/Idris/Desugar.idr +++ b/src/Idris/Desugar.idr @@ -499,11 +499,11 @@ mutual (case ws of [] => rhs' _ => ILocal fc (concat ws) rhs') - desugarClause ps arg (MkWithClause fc lhs wval cs) + desugarClause ps arg (MkWithClause fc lhs wval flags cs) = do cs' <- traverse (desugarClause ps arg) cs (bound, blhs) <- bindNames arg !(desugar LHS ps lhs) wval' <- desugar AnyExpr (bound ++ ps) wval - pure $ WithClause fc blhs wval' cs' + pure $ WithClause fc blhs wval' flags cs' desugarClause ps arg (MkImpossible fc lhs) = do dlhs <- desugar LHS ps lhs pure $ ImpossibleClause fc (snd !(bindNames arg dlhs)) @@ -624,8 +624,8 @@ mutual toIDef : ImpClause -> Core ImpDecl toIDef (PatClause fc lhs rhs) = pure $ IDef fc !(getFn lhs) [PatClause fc lhs rhs] - toIDef (WithClause fc lhs rhs cs) - = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs cs] + toIDef (WithClause fc lhs rhs flags cs) + = pure $ IDef fc !(getFn lhs) [WithClause fc lhs rhs flags cs] toIDef (ImpossibleClause fc lhs) = pure $ IDef fc !(getFn lhs) [ImpossibleClause fc lhs] diff --git a/src/Idris/Elab/Implementation.idr b/src/Idris/Elab/Implementation.idr index 4ab7f1059..92ed2d6b0 100644 --- a/src/Idris/Elab/Implementation.idr +++ b/src/Idris/Elab/Implementation.idr @@ -403,10 +403,10 @@ elabImplementation {vars} fc vis opts_in pass env nest is cons iname ps impln nu updateClause ns (PatClause fc lhs rhs) = do lhs' <- updateApp ns lhs pure (PatClause fc lhs' rhs) - updateClause ns (WithClause fc lhs wval cs) + updateClause ns (WithClause fc lhs wval flags cs) = do lhs' <- updateApp ns lhs cs' <- traverse (updateClause ns) cs - pure (WithClause fc lhs' wval cs') + pure (WithClause fc lhs' wval flags cs') updateClause ns (ImpossibleClause fc lhs) = do lhs' <- updateApp ns lhs pure (ImpossibleClause fc lhs') diff --git a/src/Idris/Elab/Interface.idr b/src/Idris/Elab/Interface.idr index 16b32f1eb..92935c0cc 100644 --- a/src/Idris/Elab/Interface.idr +++ b/src/Idris/Elab/Interface.idr @@ -395,9 +395,9 @@ elabInterface {vars} fc vis env nest constraints iname params dets mcon body changeName : Name -> ImpClause -> ImpClause changeName dn (PatClause fc lhs rhs) = PatClause fc (changeNameTerm dn lhs) rhs - changeName dn (WithClause fc lhs wval cs) + changeName dn (WithClause fc lhs wval flags cs) = WithClause fc (changeNameTerm dn lhs) wval - (map (changeName dn) cs) + flags (map (changeName dn) cs) changeName dn (ImpossibleClause fc lhs) = ImpossibleClause fc (changeNameTerm dn lhs) diff --git a/src/Idris/Parser.idr b/src/Idris/Parser.idr index e4ff634c3..36aa639d4 100644 --- a/src/Idris/Parser.idr +++ b/src/Idris/Parser.idr @@ -859,6 +859,13 @@ tyDecl fname indents atEnd indents pure (MkPTy (MkFC fname start end) n doc ty) +withFlags : SourceEmptyRule (List WithFlag) +withFlags + = do pragma "syntactic" + fs <- withFlags + pure $ Syntactic :: fs + <|> pure [] + mutual parseRHS : (withArgs : Nat) -> FileName -> FilePos -> Int -> @@ -873,11 +880,12 @@ mutual pure (MkPatClause (MkFC fname start end) lhs rhs ws) <|> do keyword "with" wstart <- location + flags <- withFlags symbol "(" wval <- bracketedExpr fname wstart indents ws <- nonEmptyBlock (clause (S withArgs) fname) end <- location - pure (MkWithClause (MkFC fname start end) lhs wval ws) + pure (MkWithClause (MkFC fname start end) lhs wval flags ws) <|> do keyword "impossible" atEnd indents end <- location diff --git a/src/Idris/REPL.idr b/src/Idris/REPL.idr index 0b53af754..96b29ebe4 100644 --- a/src/Idris/REPL.idr +++ b/src/Idris/REPL.idr @@ -188,7 +188,7 @@ printClause l i (PatClause _ lhsraw rhsraw) = do lhs <- pterm lhsraw rhs <- pterm rhsraw pure (relit l (pack (replicate i ' ') ++ show lhs ++ " = " ++ show rhs)) -printClause l i (WithClause _ lhsraw wvraw csraw) +printClause l i (WithClause _ lhsraw wvraw flags csraw) = do lhs <- pterm lhsraw wval <- pterm wvraw cs <- traverse (printClause l (i + 2)) csraw diff --git a/src/Idris/Resugar.idr b/src/Idris/Resugar.idr index 8dc07b1c8..0d2843281 100644 --- a/src/Idris/Resugar.idr +++ b/src/Idris/Resugar.idr @@ -312,9 +312,10 @@ mutual = pure (MkPatClause fc !(toPTerm startPrec lhs) !(toPTerm startPrec rhs) []) - toPClause (WithClause fc lhs rhs cs) + toPClause (WithClause fc lhs rhs flags cs) = pure (MkWithClause fc !(toPTerm startPrec lhs) !(toPTerm startPrec rhs) + flags !(traverse toPClause cs)) toPClause (ImpossibleClause fc lhs) = pure (MkImpossible fc !(toPTerm startPrec lhs)) diff --git a/src/Idris/Syntax.idr b/src/Idris/Syntax.idr index bff42c2d3..cbee738ae 100644 --- a/src/Idris/Syntax.idr +++ b/src/Idris/Syntax.idr @@ -145,7 +145,7 @@ mutual MkPatClause : FC -> (lhs : PTerm) -> (rhs : PTerm) -> (whereblock : List PDecl) -> PClause MkWithClause : FC -> (lhs : PTerm) -> (wval : PTerm) -> - List PClause -> PClause + List WithFlag -> List PClause -> PClause MkImpossible : FC -> (lhs : PTerm) -> PClause public export @@ -352,7 +352,7 @@ showCount = elimSemi mutual showAlt : PClause -> String showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";" - showAlt (MkWithClause _ lhs wval cs) = " | <>;" + showAlt (MkWithClause _ lhs wval flags cs) = " | <>;" showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;" showDo : PDo -> String @@ -405,7 +405,7 @@ mutual where showAlt : PClause -> String showAlt (MkPatClause _ lhs rhs _) = " | " ++ show lhs ++ " => " ++ show rhs ++ ";" - showAlt (MkWithClause _ lhs rhs _) = " | <>" + showAlt (MkWithClause _ lhs rhs flags _) = " | <>" showAlt (MkImpossible _ lhs) = " | " ++ show lhs ++ " impossible;" showPrec _ (PCase _ tm cs) = "case " ++ show tm ++ " of { " ++ @@ -413,7 +413,7 @@ mutual where showCase : PClause -> String showCase (MkPatClause _ lhs rhs _) = show lhs ++ " => " ++ show rhs - showCase (MkWithClause _ lhs rhs _) = " | <>" + showCase (MkWithClause _ lhs rhs flags _) = " | <>" showCase (MkImpossible _ lhs) = show lhs ++ " impossible" showPrec d (PLocal _ ds sc) -- We'll never see this when displaying a normal form... = "let { << definitions >> } in " ++ showPrec d sc @@ -812,9 +812,10 @@ mapPTermM f = goPTerm where MkPatClause fc <$> goPTerm lhs <*> goPTerm rhs <*> goPDecls wh - goPClause (MkWithClause fc lhs wVal cls) = + goPClause (MkWithClause fc lhs wVal flags cls) = MkWithClause fc <$> goPTerm lhs <*> goPTerm wVal + <*> pure flags <*> goPClauses cls goPClause (MkImpossible fc lhs) = MkImpossible fc <$> goPTerm lhs diff --git a/src/TTImp/Elab/Case.idr b/src/TTImp/Elab/Case.idr index 638f7d124..b1705bb17 100644 --- a/src/TTImp/Elab/Case.idr +++ b/src/TTImp/Elab/Case.idr @@ -328,11 +328,11 @@ caseBlock {vars} rigc elabinfo fc nest env scr scrtm scrty caseRig alts expected (bindCaseLocals loc' (map getNestData (names nest)) (reverse ns) rhs) -- With isn't allowed in a case block but include for completeness - updateClause casen splitOn nest env (WithClause loc' lhs wval cs) + updateClause casen splitOn nest env (WithClause loc' lhs wval flags cs) = let (_, args) = addEnv 0 env (usedIn lhs) args' = mkSplit splitOn lhs args lhs' = apply (IVar loc' casen) args' in - WithClause loc' (applyNested nest lhs') wval cs + WithClause loc' (applyNested nest lhs') wval flags cs updateClause casen splitOn nest env (ImpossibleClause loc' lhs) = let (_, args) = addEnv 0 env (usedIn lhs) args' = mkSplit splitOn lhs args diff --git a/src/TTImp/Interactive/GenerateDef.idr b/src/TTImp/Interactive/GenerateDef.idr index b76082e08..343a7b6c5 100644 --- a/src/TTImp/Interactive/GenerateDef.idr +++ b/src/TTImp/Interactive/GenerateDef.idr @@ -82,7 +82,7 @@ expandClause loc n c updateRHS : ImpClause -> RawImp -> ImpClause updateRHS (PatClause fc lhs _) rhs = PatClause fc lhs rhs -- 'with' won't happen, include for completeness - updateRHS (WithClause fc lhs wval cs) rhs = WithClause fc lhs wval cs + updateRHS (WithClause fc lhs wval flags cs) rhs = WithClause fc lhs wval flags cs updateRHS (ImpossibleClause fc lhs) _ = ImpossibleClause fc lhs dropLams : {vars : _} -> @@ -143,7 +143,7 @@ generateSplits : {auto m : Ref MD Metadata} -> FC -> Int -> ImpClause -> Core (List (Name, List ImpClause)) generateSplits loc fn (ImpossibleClause fc lhs) = pure [] -generateSplits loc fn (WithClause fc lhs wval cs) = pure [] +generateSplits loc fn (WithClause fc lhs wval flags cs) = pure [] generateSplits {c} {m} {u} loc fn (PatClause fc lhs rhs) = do (lhstm, _) <- elabTerm fn (InLHS linear) [] (MkNested []) [] diff --git a/src/TTImp/Parser.idr b/src/TTImp/Parser.idr index 351f9e422..6a89e4f95 100644 --- a/src/TTImp/Parser.idr +++ b/src/TTImp/Parser.idr @@ -502,7 +502,7 @@ mutual ws <- nonEmptyBlock (clause (S withArgs) fname) end <- location let fc = MkFC fname start end - pure (!(getFn lhs), WithClause fc lhs wval (map snd ws)) + pure (!(getFn lhs), WithClause fc lhs wval [] (map snd ws)) <|> do keyword "impossible" atEnd indents diff --git a/src/TTImp/ProcessDef.idr b/src/TTImp/ProcessDef.idr index 0c6fdb6e7..533af2ecc 100644 --- a/src/TTImp/ProcessDef.idr +++ b/src/TTImp/ProcessDef.idr @@ -78,15 +78,11 @@ export impossibleErrOK : {auto c : Ref Ctxt Defs} -> Defs -> Error -> Core Bool impossibleErrOK defs (CantConvert fc env l r) - = do logTerm 10 "Impossible" !(normalise defs env l) - logTerm 10 " ...and" !(normalise defs env r) - impossibleOK defs !(nf defs env l) - !(nf defs env r) + = impossibleOK defs !(nf defs env l) + !(nf defs env r) impossibleErrOK defs (CantSolveEq fc env l r) - = do logTerm 10 "Impossible" !(normalise defs env l) - logTerm 10 " ...and" !(normalise defs env r) - impossibleOK defs !(nf defs env l) - !(nf defs env r) + = impossibleOK defs !(nf defs env l) + !(nf defs env r) impossibleErrOK defs (BadDotPattern _ _ ErasedArg _ _) = pure True impossibleErrOK defs (CyclicMeta _ _ _ _) = pure True impossibleErrOK defs (AllFailed errs) @@ -122,15 +118,11 @@ export recoverableErr : {auto c : Ref Ctxt Defs} -> Defs -> Error -> Core Bool recoverableErr defs (CantConvert fc env l r) - = do logTerm 10 "Impossible" !(normalise defs env l) - logTerm 10 " ...and" !(normalise defs env r) - recoverable defs !(nf defs env l) - !(nf defs env r) + = recoverable defs !(nf defs env l) + !(nf defs env r) recoverableErr defs (CantSolveEq fc env l r) - = do logTerm 10 "Impossible" !(normalise defs env l) - logTerm 10 " ...and" !(normalise defs env r) - recoverable defs !(nf defs env l) - !(nf defs env r) + = recoverable defs !(nf defs env l) + !(nf defs env r) recoverableErr defs (BadDotPattern _ _ ErasedArg _ _) = pure True recoverableErr defs (CyclicMeta _ _ _ _) = pure True recoverableErr defs (AllFailed errs) @@ -453,7 +445,7 @@ checkClause {vars} mult hashit n opts nest env (PatClause fc lhs_in rhs) pure (Right (MkClause env' lhstm' rhstm)) -- TODO: (to decide) With is complicated. Move this into its own module? -checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs) +checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw flags cs) = do (lhs, (vars' ** (sub', env', nest', lhspat, reqty))) <- checkLHS False mult hashit n opts nest env fc lhs_in let wmode @@ -492,9 +484,12 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs let notreqns = fst bnr let notreqty = snd bnr - wtyScope <- replace defs scenv !(nf defs scenv (weaken wval)) + rdefs <- if Syntactic `elem` flags + then clearDefs defs + else pure defs + wtyScope <- replace rdefs scenv !(nf rdefs scenv (weaken wval)) (Local fc (Just False) _ First) - !(nf defs scenv + !(nf rdefs scenv (weaken {n=wargn} notreqty)) let bNotReq = Bind fc wargn (Pi top Explicit wvalTy) wtyScope @@ -567,11 +562,11 @@ checkClause {vars} mult hashit n opts nest env (WithClause fc lhs_in wval_raw cs = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs newrhs <- withRHS ploc drop wname wargnames rhs lhs pure (PatClause ploc newlhs newrhs) - mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs ws) + mkClauseWith drop wname wargnames lhs (WithClause ploc patlhs rhs flags ws) = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs newrhs <- withRHS ploc drop wname wargnames rhs lhs ws' <- traverse (mkClauseWith (S drop) wname wargnames lhs) ws - pure (WithClause ploc newlhs newrhs ws') + pure (WithClause ploc newlhs newrhs flags ws') mkClauseWith drop wname wargnames lhs (ImpossibleClause ploc patlhs) = do newlhs <- getNewLHS ploc drop nest wname wargnames lhs patlhs pure (ImpossibleClause ploc newlhs) diff --git a/src/TTImp/TTImp.idr b/src/TTImp/TTImp.idr index 5293a47e5..a15035282 100644 --- a/src/TTImp/TTImp.idr +++ b/src/TTImp/TTImp.idr @@ -292,10 +292,19 @@ mutual " " ++ show con ++ "\n\t" ++ showSep "\n\t" (map show fields) ++ "\n" + public export + data WithFlag + = Syntactic -- abstract syntactically, rather than by value + + export + Eq WithFlag where + Syntactic == Syntactic = True + public export data ImpClause : Type where PatClause : FC -> (lhs : RawImp) -> (rhs : RawImp) -> ImpClause WithClause : FC -> (lhs : RawImp) -> (wval : RawImp) -> + (flags : List WithFlag) -> List ImpClause -> ImpClause ImpossibleClause : FC -> (lhs : RawImp) -> ImpClause @@ -303,7 +312,7 @@ mutual Show ImpClause where show (PatClause fc lhs rhs) = show lhs ++ " = " ++ show rhs - show (WithClause fc lhs wval block) + show (WithClause fc lhs wval flags block) = show lhs ++ " with " ++ show wval ++ "\n\t" ++ show block show (ImpossibleClause fc lhs) = show lhs ++ " impossible" @@ -835,7 +844,7 @@ mutual = do tag 0; toBuf b fc; toBuf b lhs; toBuf b rhs toBuf b (ImpossibleClause fc lhs) = do tag 1; toBuf b fc; toBuf b lhs - toBuf b (WithClause fc lhs wval cs) + toBuf b (WithClause fc lhs wval flags cs) = do tag 2; toBuf b fc; toBuf b lhs; toBuf b wval; toBuf b cs fromBuf b @@ -847,7 +856,7 @@ mutual pure (ImpossibleClause fc lhs) 2 => do fc <- fromBuf b; lhs <- fromBuf b; wval <- fromBuf b; cs <- fromBuf b - pure (WithClause fc lhs wval cs) + pure (WithClause fc lhs wval [] cs) _ => corrupt "ImpClause" export diff --git a/src/TTImp/Utils.idr b/src/TTImp/Utils.idr index 16904ccc8..e8a533cfc 100644 --- a/src/TTImp/Utils.idr +++ b/src/TTImp/Utils.idr @@ -150,11 +150,11 @@ mutual ++ bound in PatClause fc (substNames [] [] lhs) (substNames bound' ps rhs) - substNamesClause bound ps (WithClause fc lhs wval cs) + substNamesClause bound ps (WithClause fc lhs wval flags cs) = let bound' = map UN (map snd (findBindableNames True bound [] lhs)) ++ bound in WithClause fc (substNames [] [] lhs) - (substNames bound' ps wval) cs + (substNames bound' ps wval) flags cs substNamesClause bound ps (ImpossibleClause fc lhs) = ImpossibleClause fc (substNames bound [] lhs) @@ -230,9 +230,10 @@ mutual substLocClause fc' (PatClause fc lhs rhs) = PatClause fc' (substLoc fc' lhs) (substLoc fc' rhs) - substLocClause fc' (WithClause fc lhs wval cs) + substLocClause fc' (WithClause fc lhs wval flags cs) = WithClause fc' (substLoc fc' lhs) (substLoc fc' wval) + flags (map (substLocClause fc') cs) substLocClause fc' (ImpossibleClause fc lhs) = ImpossibleClause fc' (substLoc fc' lhs) diff --git a/tests/ideMode/ideMode001/expected b/tests/ideMode/ideMode001/expected index 2c1ed8a26..ab645029f 100644 --- a/tests/ideMode/ideMode001/expected +++ b/tests/ideMode/ideMode001/expected @@ -8,7 +8,7 @@ 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1) 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1) 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1) -0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:759:1--766:1 n[2] m[4]) a[3])))")))))) 1) +0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1) 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) diff --git a/tests/ideMode/ideMode003/expected b/tests/ideMode/ideMode003/expected index 7472997c2..c138545a3 100644 --- a/tests/ideMode/ideMode003/expected +++ b/tests/ideMode/ideMode003/expected @@ -8,7 +8,7 @@ 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 7 18) (:end 7 21)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:265}_[] ?{_:264}_[])")))))) 1) 0000d8(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 16) (:end 7 1)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect m a)")))))) 1) 0000ed(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 6 11) (:end 6 14)) ((:name "ys") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "(Main.Vect ?{_:254}_[] ?{_:253}_[])")))))) 1) -0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:759:1--766:1 n[2] m[4]) a[3])))")))))) 1) +0001ca(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 1) (:end 6 1)) ((:name "Main.append") (:namespace "") (:decor :bound) (:implicit :False) (:key "") (:doc-overview "") (:type "{0 m : Prelude.Nat} -> {0 a : Type} -> {0 n : Prelude.Nat} -> (({arg:244} : (Main.Vect n[0] a[1])) -> (({arg:245} : (Main.Vect m[3] a[2])) -> (Main.Vect (Prelude.+ Prelude.Nat Prelude.Num implementation at Prelude.idr:761:1--768:1 n[2] m[4]) a[3])))")))))) 1) 0000cb(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 47) (:end 6 1)) ((:name "a") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Type")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 44) (:end 5 45)) ((:name "m") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1) 0000d3(:output (:ok (:highlight-source ((((:filename "LocType.idr") (:start 5 40) (:end 5 42)) ((:name "n") (:namespace "") (:decor :type) (:implicit :False) (:key "") (:doc-overview "") (:type "Prelude.Nat")))))) 1)