idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-12-01 01:09:03 +03:00
Code Issues Projects Releases Wiki Activity

Merge pull request #196 from edwinb/with-experiment

Browse Source 
Experiment %syntactic flag on with
This commit is contained in:
Edwin Brady 2020-05-29 17:01:41 +01:00 committed by GitHub
commit 843b30b4d1
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
17 changed files with 71 additions and 50 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
libs/base/Data/IORef.idr
View File

@ -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)

4
libs/prelude/Prelude.idr
View File

@ -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

8
src/Idris/Desugar.idr
View File

@ -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]

4
src/Idris/Elab/Implementation.idr
View File

@ -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')

4
src/Idris/Elab/Interface.idr
View File

@ -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)

10
src/Idris/Parser.idr
View File

@ -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

2
src/Idris/REPL.idr
View File

@ -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

3
src/Idris/Resugar.idr
View File

@ -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))

11
src/Idris/Syntax.idr
View File

@ -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) = " | <<with alts not possible>>;"
showAlt (MkWithClause _ lhs wval flags cs) = " | <<with alts not possible>>;"
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 _) = " | <<with alts not possible>>"
showAlt (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
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 _) = " | <<with alts not possible>>"
showCase (MkWithClause _ lhs rhs flags _) = " | <<with alts not possible>>"
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

4
src/TTImp/Elab/Case.idr
View File

@ -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

4
src/TTImp/Interactive/GenerateDef.idr
View File

@ -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 []) []

2
src/TTImp/Parser.idr
View File

@ -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

37
src/TTImp/ProcessDef.idr
View File

@ -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)

15
src/TTImp/TTImp.idr
View File

@ -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

7
src/TTImp/Utils.idr
View File

@ -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)

2
tests/ideMode/ideMode001/expected
View File

@ -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)

2
tests/ideMode/ideMode003/expected
View File

@ -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)