msmorgan

module Text.Lexer.Bikeshedding

{-
Other choices include:

-:, $:
!=>, $=>
:>, :$>
#^, *! -- not really

msmorgan

||| Utilities functions for contitionally delaying values.
module Control.Delayed

%default total

||| Type-level function for a conditionally infinite type.
public export
inf : Bool -> Type -> Type
inf True a = Inf a
inf False a = a

msmorgan

||| Recognises JSON string literals.
module Language.JSON.String

import Data.String.Extra
import Text.Lexer
import Text.Lexer.Util
import Text.Parser

%default total
%access private

msmorgan

module Data.String.Extra

%access public export
%default total

||| Remove the first `n` characters from a string. Returns the empty string if
||| the input string is too short.
drop : (n : Nat) -> (input : String) -> String
drop n str = substr n (length str) str

msmorgan

module Control.ChainedComparison

%default total
%access export

public export
data Direction = Ascending | Descending

data ComparisonChain : Direction -> Type -> Type where
  Vacuous : ComparisonChain d ty

msmorgan

module ComparisonChain

%access public export

infixl 6 |==|, |/=|
infixl 6 |<|, |<=|, |>=|, |>|

namespace Interfaces
  interface ChainEq ty where
    (|==|) : ty -> ty -> Bool

msmorgan

module InfixrBooleanOps

%default total

factorial : Nat -> Integer
factorial Z = 1
factorial (S n) = (cast (S n)) * factorial n

infixr 4 &&>, ||>

msmorgan

module MyModule

import Text.Parser

%hide Prelude.Applicative.(<|>)
%rename Text.Parser.(<||>) (<|>)

msmorgan

module NotElem

import Data.Vect

%default Total

NotElem : (x : a) -> Vect n a -> Type
NotElem x ys = Not (Elem x ys)

notElem : DecEq a => (x : a) -> (ys : Vect n a) -> Dec (NotElem x ys)

msmorgan

module Triv

import Data.Vect

%default total

triv : {x : a} -> a
triv {x} = x

oneTwoThree : (n ** Vect n Nat)