mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
fixed whitespace for *.idr,*.ipkg,*.tex,*.yaff, and *.lidr
This commit is contained in:
parent
e15b1f0c78
commit
a52fbfb096
@ -7,4 +7,3 @@ modules = Text.Readline
|
||||
prebuild = "make -C readline_glue"
|
||||
postinstall = "make -C readline_glue install"
|
||||
postclean = "make -C readline_glue clean"
|
||||
|
||||
|
@ -2,4 +2,3 @@
|
||||
-- interactive editing modes for the Idris 2 code here!
|
||||
|
||||
package dummy
|
||||
|
||||
|
@ -2,4 +2,3 @@
|
||||
-- interactive editing modes for the Idris 2 code here!
|
||||
|
||||
package dummy
|
||||
|
||||
|
@ -2,4 +2,3 @@
|
||||
-- interactive editing modes for the Idris 2 code here!
|
||||
|
||||
package proof
|
||||
|
||||
|
@ -9,4 +9,3 @@
|
||||
> = case xs of
|
||||
> [] => ?bar_3
|
||||
> (x :: zs) => ?bar_4
|
||||
|
||||
|
@ -62,7 +62,7 @@ interp : Env $gam -> Lang $gam $t -> interpTy $t
|
||||
interp $env (Var $i) = lookupEnv i env
|
||||
interp $env (Val $x) = x
|
||||
interp $env (App $f $a) = interp env f (interp env a)
|
||||
interp $env (Lam {s = $s} $scope)
|
||||
interp $env (Lam {s = $s} $scope)
|
||||
= \var => interp (ECons var env) scope
|
||||
interp $env (Op $fn $x $y) = fn (interp env x) (interp env y)
|
||||
|
||||
|
@ -62,7 +62,7 @@ interp : Env $gam -> Lang $gam $t -> interpTy $t
|
||||
interp $env (Var $i) = lookupEnv i env
|
||||
interp $env (Val $x) = x
|
||||
interp $env (App $f $a) = interp env f (interp env a)
|
||||
interp $env (Lam {s = $s} $scope)
|
||||
interp $env (Lam {s = $s} $scope)
|
||||
= \var => interp (ECons var env) scope
|
||||
interp $env (Op $fn $x $y) = fn (interp env x) (interp env y)
|
||||
|
||||
|
@ -52,7 +52,7 @@ data Infer : Type where
|
||||
MkInfer : $a -> Infer
|
||||
|
||||
long : Infer
|
||||
long
|
||||
long
|
||||
= MkInfer (Vect.Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
||||
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
||||
Cons 0 (Cons 0 (Cons 0 (Cons 0 (Cons 0 (
|
||||
|
@ -31,7 +31,7 @@ namespace Vect
|
||||
data Maybe : Type -> Type where
|
||||
Nothing : Maybe $a
|
||||
Just : $a -> Maybe $a
|
||||
|
||||
|
||||
testMaybe : Maybe (Vect ? Integer)
|
||||
testMaybe = Just (Cons 1 Nil)
|
||||
|
||||
|
@ -25,4 +25,3 @@ zip : Vect n a -> Vect n b -> Vect n (Pair a b)
|
||||
zip Nil (Cons _ _) impossible
|
||||
zip Nil Nil = Nil
|
||||
zip (Cons x xs) (Cons y ys) = Cons (MkPair x y) (zip xs ys)
|
||||
|
||||
|
@ -24,4 +24,3 @@ data Pair : Type -> Type -> Type where
|
||||
zip : Vect n a -> Vect n b -> Vect n (Pair a b)
|
||||
zip Nil Nil impossible
|
||||
zip (Cons x xs) (Cons y ys) = Cons (MkPair x y) (zip xs ys)
|
||||
|
||||
|
@ -25,4 +25,3 @@ zip : Vect n a -> Vect n b -> Vect n (Pair a b)
|
||||
zip Nil Z impossible
|
||||
zip Nil Nil = Nil
|
||||
zip (Cons x xs) (Cons y ys) = Cons (MkPair x y) (zip xs ys)
|
||||
|
||||
|
@ -19,4 +19,3 @@ data Baz : Nat -> Type where
|
||||
|
||||
addBaz : (x : Nat) -> Baz x -> Nat
|
||||
addBaz (plus $x $y) (AddThings $x $y) = plus x y
|
||||
|
||||
|
@ -16,4 +16,3 @@ addBaz (plus x y) (AddThings x y) = plus x y
|
||||
-- which would accidentally lead to a non-linear pattern
|
||||
addBaz3 : (x : Nat) -> Baz x -> Nat
|
||||
addBaz3 (plus x x) (AddThings _ _) = plus x x
|
||||
|
||||
|
@ -15,4 +15,3 @@ addBaz (plus x y) (AddThings _ _) = plus x y
|
||||
-- Can't unify because of the repeated argument
|
||||
addBaz4 : (x : Nat) -> Baz x -> Nat
|
||||
addBaz4 (plus _ _) (AddThings x x) = plus x x
|
||||
|
||||
|
@ -24,4 +24,3 @@ take (S $k) (Cons $x $xs) = Cons x (take k (Force xs))
|
||||
every2nd : Nat -> Stream $a -> List $a
|
||||
every2nd Z $xs = Nil
|
||||
every2nd (S $k) (Cons _ (Delay (Cons $x $xs))) = Cons x (every2nd k (Force xs))
|
||||
|
||||
|
@ -1,6 +1,6 @@
|
||||
testlet : Integer -> Integer
|
||||
testlet $x = let y = prim__add_Integer x x in
|
||||
prim__add_Integer y y
|
||||
testlet $x = let y = prim__add_Integer x x in
|
||||
prim__add_Integer y y
|
||||
|
||||
data Nat : Type where
|
||||
Z : Nat
|
||||
@ -11,7 +11,7 @@ plus Z $y = y
|
||||
plus (S $k) $y = S (plus k y)
|
||||
|
||||
fn2 : Nat -> Nat -> Nat
|
||||
fn2 $x $y
|
||||
fn2 $x $y
|
||||
= let w : Nat
|
||||
w = plus x x;
|
||||
help : Nat -> Nat
|
||||
@ -19,7 +19,7 @@ fn2 $x $y
|
||||
plus (help y) w
|
||||
|
||||
fn : Nat -> Nat -> Nat
|
||||
fn $x $y
|
||||
fn $x $y
|
||||
= let w : ?; w = plus x x in
|
||||
let foo = plus x x in
|
||||
let help : Nat -> Nat;
|
||||
|
@ -37,4 +37,3 @@ cvec2 {n = n@(_)} $xs
|
||||
= case xs of
|
||||
Nil => n
|
||||
Cons $x $xs => n
|
||||
|
||||
|
@ -30,7 +30,7 @@ fiftythousand = mult five tenthousand
|
||||
hundredthousand : Nat
|
||||
hundredthousand = mult ten tenthousand
|
||||
|
||||
data IsSuc : Nat -> Type where
|
||||
data IsSuc : Nat -> Type where
|
||||
Yes : IsSuc (S $k)
|
||||
|
||||
nonZero : IsSuc Main.hundredthousand
|
||||
|
@ -90,4 +90,3 @@ stuff = Cons False (Cons True (Cons False (Cons True (Cons False (Cons True
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
))))))))))))))))))))))))))))))))))))))))))))))))
|
||||
|
||||
|
@ -12,4 +12,3 @@ dup2 $x = MkPair ?baz2 x
|
||||
|
||||
dupbad : (1 x : $a) -> Pair $a $a
|
||||
dupbad $x = MkPair x x
|
||||
|
||||
|
@ -1,7 +1,7 @@
|
||||
data Eq : $a -> $b -> Type where
|
||||
Refl : Eq $x $x
|
||||
|
||||
okay : {p : $a -> Type} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) ->
|
||||
okay : {p : $a -> Type} -> (1 x : $a) -> (1 y : $a) -> (1 prf : Eq x y) ->
|
||||
p x -> p y
|
||||
-- Should fail on the LHS, before even getting to the RHS, because
|
||||
-- after elaboration 'x' appears twice even though it is linearly bound.
|
||||
|
@ -39,7 +39,7 @@ testPair : MyDPair Nat (\n => Vect n Integer)
|
||||
testPair = MkMyDPair _ (Cons 1 (Cons 2 (Cons 3 Nil)))
|
||||
|
||||
testDVect : DVect Integer
|
||||
testDVect = MkDVect 94 (Cons 1 (Cons 2 (Cons 3 Nil)))
|
||||
testDVect = MkDVect 94 (Cons 1 (Cons 2 (Cons 3 Nil)))
|
||||
|
||||
testPerson : Person
|
||||
testPerson = MkPerson "Wowbagger" 1337 10 (\x => S x)
|
||||
|
@ -44,4 +44,3 @@ testPerson = MkPerson "Fred" 1337 10 (MkStats 10 10)
|
||||
|
||||
grow : Person -> Person
|
||||
grow p = record { more->height $= prim__add_Integer 1 } p
|
||||
|
||||
|
@ -26,10 +26,9 @@ UTForASCII ASCII = Nat -- Just as demonstration
|
||||
record FlexiString { default UTF k : KindOfString} where
|
||||
constructor MkFlexiString
|
||||
val : UTForASCII k
|
||||
|
||||
|
||||
c : FlexiString
|
||||
c = MkFlexiString "hello"
|
||||
|
||||
d : FlexiString {k = ASCII}
|
||||
d = MkFlexiString Z
|
||||
|
||||
|
@ -47,4 +47,3 @@ pfoom (C0 EPS) = Z
|
||||
pfoom (C0 (C1 x)) = S (pfoom (C0 x))
|
||||
pfoom (C0 (C0 x)) = pfoom (C0 x)
|
||||
pfoom (C1 x) = S (foom x)
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user