git.iko.soy/Idris-dev
on master help sign in
Minor change to display of metavariables
18e4b21Edwin Brady
src/Idris/Core/Elaborate.hs+4−4
compare with master
unifiedsplit
@@ -711,8 +711,8 @@ checkPiGoal n
711 = do g <- goal
711 = do g <- goal
712 case g of
712 case g of
713 Bind _ (Pi _ _ _) _ -> return ()
713 Bind _ (Pi _ _ _) _ -> return ()
714− _ -> do a <- getNameFrom (sMN 0 "pargTy")
714+ _ -> do a <- getNameFrom (sMN 0 "__pargTy")
715− b <- getNameFrom (sMN 0 "pretTy")
715+ b <- getNameFrom (sMN 0 "__pretTy")
716 f <- getNameFrom (sMN 0 "pf")
716 f <- getNameFrom (sMN 0 "pf")
717 claim a RType
717 claim a RType
718 claim b RType
718 claim b RType
@@ -725,8 +725,8 @@ checkPiGoal n
725
725
726simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
726simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()
727simple_app infer fun arg str =
727simple_app infer fun arg str =
728− do a <- getNameFrom (sMN 0 "argTy")
728+ do a <- getNameFrom (sMN 0 "__argTy")
729− b <- getNameFrom (sMN 0 "retTy")
729+ b <- getNameFrom (sMN 0 "__retTy")
730 f <- getNameFrom (sMN 0 "f")
730 f <- getNameFrom (sMN 0 "f")
731 s <- getNameFrom (sMN 0 "s")
731 s <- getNameFrom (sMN 0 "s")
732 claim a RType
732 claim a RType
src/Idris/REPL.hs+8−6
@@ -942,12 +942,14 @@ process fn (Check (PRef _ _ n))
942 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
942 putTy :: PPOption -> IState -> Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
943 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
943 putTy ppo ist 0 bnd sc = putGoal ppo ist bnd sc
944 putTy ppo ist i bnd (PPi _ n _ t sc)
944 putTy ppo ist i bnd (PPi _ n _ t sc)
945− = let current = text " " <>
945+ = let current = case n of
946− (case n of
947− MN _ _ -> text "_"
946+ MN _ _ -> text ""
948− UN nm | ('_':'_':_) <- str nm -> text "_"
947+ UN nm | ('_':'_':_) <- str nm -> text ""
948+ _ -> text " " <>
949− _ -> bindingOf n False) <+>
949+ bindingOf n False
950+ <+> colon
950− colon <+> align (tPretty bnd ist t) <> line
951+ <+> align (tPretty bnd ist t)
952+ <> line
951 in
953 in
952 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
954 current <> putTy ppo ist (i-1) ((n,False):bnd) sc
953 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc
955 putTy ppo ist _ bnd sc = putGoal ppo ist ((n,False):bnd) sc