git.iko.soy/Idris-dev
on master help sign in
Display tweak
7a5392dEdwin Brady
libs/base/Data/VectType.idr+3−3
compare with master
unifiedsplit
@@ -14,9 +14,9 @@ infixr 7 ::
14data Vect : Nat -> Type -> Type where
14data Vect : Nat -> Type -> Type where
15 ||| Empty vector
15 ||| Empty vector
16 Nil : Vect Z a
16 Nil : Vect Z a
17− ||| A non-empty vector of length `S n`, consisting of a head element and
17+ ||| A non-empty vector of length `S k`, consisting of a head element and
18− ||| the rest of the list, of length `n`.
18+ ||| the rest of the list, of length `k`.
19− (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
19+ (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
20
20
21-- Hints for interactive editing
21-- Hints for interactive editing
22%name Vect xs,ys,zs,ws
22%name Vect xs,ys,zs,ws
src/Idris/AbsSyntaxTree.hs+3−1
@@ -1574,7 +1574,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd
1574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
1575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
1576 where
1576 where
1577+ uname (UN n) = case str n of
1578+ ('_':_) -> False
1577− uname (UN _) = True
1579+ _ -> True
1578 uname _ = False
1580 uname _ = False
1579
1581
1580 st =
1582 st =