mirror of
https://github.com/sharkdp/bat.git
synced 2025-02-13 08:28:57 +00:00
108 lines
1.6 KiB
Idris
Vendored
108 lines
1.6 KiB
Idris
Vendored
-- some code in Idris
|
|
module XX.X'''
|
|
|
|
import Data.Nat
|
|
|
|
data X = A | B
|
|
|
|
namespace X
|
|
||| Documentation
|
|
record Y where
|
|
[noHints]
|
|
constructor MkY'
|
|
field1 : Nat
|
|
{auto x : Nat}
|
|
|
|
namespace X' {
|
|
parameters (x : A (Maybe b))
|
|
x : Nat
|
|
}
|
|
|
|
u : ()
|
|
u = ()
|
|
|
|
k, w, u : Char
|
|
k = '\NUL'
|
|
w = 'w'
|
|
|
|
x = [1, 0, 3, "sdf\{d}", 0xFF, 0o77, 0b10_1, 100_100]
|
|
|
|
f : Int -> Int
|
|
f = if x > 0 then x else 0 () SS `elem` S $ do
|
|
x <- a [1, 2, 3]
|
|
let ukuk = akak
|
|
rewrite $ Wow Wow Wow Wow.Wow b W (W)
|
|
pure $ f A B c D (EE) E
|
|
|
|
(&&&) : Nat -> Nat -> Nat
|
|
z &&& y = d + ?foo
|
|
(&&&) x y = ?asfda
|
|
|
|
public export covering
|
|
(.fun) : X a Y b => Nat -> Nat
|
|
Z .fun = haha.fun haha .N
|
|
(.fun) Z = ahah $ \case
|
|
x@(x, y) => Prelude.Types.ahahah
|
|
|
|
(.N) : Nat -> Nat
|
|
Z .N = Z
|
|
(.N) (S n) = (.N) n
|
|
|
|
xx : Name
|
|
xx = `{Full.Name}
|
|
|
|
infixr 0 ^^^, &&&
|
|
|
|
xxx : ?
|
|
xxx = case x of
|
|
Z => lalalaCamelCase
|
|
z => alalalCamelCase
|
|
|
|
ff : Nat -> TTImp
|
|
ff 0 = let x = 0 in val
|
|
ff _ = `(let x = 0 in ~val ^~^ ~(abc))
|
|
ff _ = f `(let x = 0 in ~val ^~^ ~(abc)) x
|
|
|
|
%language ElabReflection
|
|
%runElab X.sf ads
|
|
|
|
%macro %inline
|
|
fff : List Decl
|
|
fff = `[
|
|
f : Nat -> Nat
|
|
|
|
f Z = haha %runElab %search @{%World}
|
|
]
|
|
|
|
private infixr 4 ^--^
|
|
|
|
(^--^) : Nat -> Nat -> Nat
|
|
(^--^) Z Z = Z
|
|
x ^--^ y = x + y
|
|
|
|
x : (y : Vect n (Maybe (Maybe (&&&) Nat))) ->
|
|
{x : Nat} -> {auto _ : Monoid a} ->
|
|
{default 4 xx : Nat} ->
|
|
{default (f x Y) xx' : Nat} ->
|
|
String
|
|
x Z S = ?foo
|
|
x y _ = "a b \{show $ let x = 0 in y} y >>= z"
|
|
|
|
multiline : String
|
|
multiline = """
|
|
A multiline string\NUL
|
|
"""
|
|
|
|
f' : Nat -> Nat
|
|
f' = x' 4
|
|
|
|
x : Char
|
|
x = '\BEL'
|
|
x = '\\'
|
|
x = '\''
|
|
x = '\o755'
|
|
x = 'a'
|
|
|
|
xx : Int
|
|
xx = 0o7_5_5
|