mirror of
https://github.com/anoma/juvix.git
synced 2024-11-30 05:42:26 +03:00
parent
ae89c4d480
commit
e951df077d
@ -25,4 +25,4 @@ resultHeading : String := "Collatz sequence:";
|
||||
|
||||
main : IO :=
|
||||
printStringLn welcome
|
||||
>>> readLn λ {s := printStringLn resultHeading >>> run collatz (stringToNat s)};
|
||||
>>> readLn λ{s := printStringLn resultHeading >>> run collatz (stringToNat s)};
|
||||
|
@ -854,10 +854,10 @@ instance (SingI s) => PrettyPrint (Lambda s) where
|
||||
ppCode Lambda {..} = do
|
||||
let lambdaKw' = ppCode _lambdaKw
|
||||
braces' = uncurry enclose (over both ppCode (_lambdaBraces ^. unIrrelevant))
|
||||
lambdaClauses' = case _lambdaClauses of
|
||||
s :| [] -> braces' (ppCode s)
|
||||
_ -> braces' (blockIndent (vsepHard (ppCode <$> _lambdaClauses)))
|
||||
lambdaKw' <+> lambdaClauses'
|
||||
lambdaClauses' = braces' $ case _lambdaClauses of
|
||||
s :| [] -> ppCode s
|
||||
_ -> blockIndent (vsepHard (ppCode <$> _lambdaClauses))
|
||||
lambdaKw' <> lambdaClauses'
|
||||
|
||||
instance PrettyPrint Precedence where
|
||||
ppCode = \case
|
||||
|
@ -167,7 +167,7 @@ exampleFunction2
|
||||
-> List A
|
||||
-> List A
|
||||
-> Nat :=
|
||||
λ {_ _ _ _ _ _ _ _ _ _ :=
|
||||
λ{_ _ _ _ _ _ _ _ _ _ :=
|
||||
undefined
|
||||
-- comment after first
|
||||
+ undefined
|
||||
@ -186,11 +186,11 @@ positive
|
||||
type T0 (A : Type) := c0 : (A -> T0 A) -> T0 A;
|
||||
|
||||
-- Single Lambda clause
|
||||
idLambda : {A : Type} -> A -> A := λ {x := x};
|
||||
idLambda : {A : Type} -> A -> A := λ{x := x};
|
||||
|
||||
-- Lambda clauses
|
||||
f : Nat -> Nat :=
|
||||
\ {
|
||||
\{
|
||||
-- comment before lambda pipe
|
||||
| zero :=
|
||||
let
|
||||
@ -305,7 +305,7 @@ module Traits;
|
||||
instance
|
||||
showBoolI : Show Bool :=
|
||||
mkShow@{
|
||||
show := λ {x := ite x "true" "false"}
|
||||
show := λ{x := ite x "true" "false"}
|
||||
};
|
||||
|
||||
instance
|
||||
|
@ -6,4 +6,4 @@ type T A := mkT@{pp : A → A};
|
||||
type Unit := unit;
|
||||
|
||||
instance
|
||||
unitI : T Unit := mkT λ {x := x};
|
||||
unitI : T Unit := mkT λ{x := x};
|
||||
|
@ -8,6 +8,6 @@ type Bool :=
|
||||
| false;
|
||||
|
||||
instance
|
||||
boolI : T Bool := mkT λ {x := x};
|
||||
boolI : T Bool := mkT λ{x := x};
|
||||
|
||||
main : Bool := case T.pp unit of unit := T.pp true;
|
||||
|
@ -3,7 +3,7 @@ module SignatureWithBody;
|
||||
import Stdlib.Prelude open;
|
||||
|
||||
isNull : {A : Type} → List A → Bool :=
|
||||
λ {
|
||||
λ{
|
||||
| nil := true
|
||||
| _ := false
|
||||
};
|
||||
@ -11,7 +11,7 @@ isNull : {A : Type} → List A → Bool :=
|
||||
isNull' : {A : Type} → List A → Bool :=
|
||||
let
|
||||
aux : {A : Type} → List A → Bool :=
|
||||
λ {
|
||||
λ{
|
||||
| nil := true
|
||||
| _ := false
|
||||
};
|
||||
|
@ -27,7 +27,7 @@ filter : (a : Type) → (a → Bool) → List a → List a
|
||||
| a f (:: h hs) :=
|
||||
match
|
||||
(f h)
|
||||
λ {
|
||||
λ{
|
||||
| true := :: h (filter a f hs)
|
||||
| false := filter a f hs
|
||||
};
|
||||
@ -65,14 +65,14 @@ splitAt : (a : Type) → ℕ → List a → List a × List a
|
||||
| a _ nil := , nil nil
|
||||
| a zero xs := , nil xs
|
||||
| a (suc zero) (:: x xs) := , (:: x nil) xs
|
||||
| a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ {(, xs' xs'') := , (:: x xs') xs''};
|
||||
| a (suc (suc m)) (:: x xs) := match (splitAt a m xs) λ{(, xs' xs'') := , (:: x xs') xs''};
|
||||
|
||||
terminating
|
||||
merge : (a : Type) → (a → a → Ordering) → List a → List a → List a
|
||||
| a cmp (:: x xs) (:: y ys) :=
|
||||
match
|
||||
(cmp x y)
|
||||
λ {
|
||||
λ{
|
||||
| LT := :: x (merge a cmp xs (:: y ys))
|
||||
| _ := :: y (merge a cmp (:: x xs) ys)
|
||||
}
|
||||
@ -92,7 +92,7 @@ quickSort : (a : Type) → (a → a → Ordering) → List a → List a
|
||||
ltx (y : a) : Bool :=
|
||||
match
|
||||
(cmp y x)
|
||||
λ {
|
||||
λ{
|
||||
| LT := true
|
||||
| _ := false
|
||||
};
|
||||
|
Loading…
Reference in New Issue
Block a user