1
0
mirror of https://github.com/sharkdp/bat.git synced 2025-02-12 16:08:38 +00:00
2025-01-27 23:47:20 +03:00

108 lines
18 KiB
Idris
Vendored
Raw Blame History

This file contains invisible Unicode characters

This file contains invisible Unicode characters that are indistinguishable to humans but may be processed differently by a computer. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

-- 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