git.iko.soy/Idris-dev
on master help sign in
Display tweak
commit7a5392d414e64ddeca75267add9ba78c17b96376 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 9 Aug 2015, 15:39 (11 years ago) parentcd0528a
2 files changed+6−4
compare with master
unifiedsplit
libs/base/Data/VectType.idr+3−3 src/Idris/AbsSyntaxTree.hs+3−1
libs/base/Data/VectType.idr+3−3
@@ -14,9 +14,9 @@ infixr 7 ::
1414data Vect : Nat -> Type -> Type where
1515 ||| Empty vector
1616 Nil : Vect Z a
17− ||| A non-empty vector of length `S n`, consisting of a head element and
18− ||| the rest of the list, of length `n`.
19− (::) : (x : a) -> (xs : Vect n a) -> Vect (S n) a
17+ ||| A non-empty vector of length `S k`, consisting of a head element and
18+ ||| the rest of the list, of length `k`.
19+ (::) : (x : a) -> (xs : Vect k a) -> Vect (S k) a
2020
2121-- Hints for interactive editing
2222%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
15741574 group (prettySe (decD d) (startPrec + 1) bnd ty <+> st) <> text "->" <$>
15751575 group (prettySe (decD d) startPrec ((n, False):bnd) sc)
15761576 where
1577− uname (UN _) = True
1577+ uname (UN n) = case str n of
1578+ ('_':_) -> False
1579+ _ -> True
15781580 uname _ = False
15791581
15801582 st =