idris2-refined: Refinement types for Idris2

This library provides predicates, combinators, and elaborator scripts for working with refinement types with a focus on refined primitives. Here is a motivating example:

module README

import Data.Refined
import Data.Refined.String
import Data.Refined.Integer
import Derive.Prelude
import Derive.Refined
import Derive.HDecEq

%default total
%language ElabReflection

public export
MaxLen : Nat
MaxLen = 50

public export
0 IsAlias : String -> Type
IsAlias = Str $ Trimmed && Len (`LTE` MaxLen) && All PrintableAscii

public export
record Alias where
  constructor MkAlias
  value : String
  {auto 0 prf : IsAlias value}

%runElab derive "Alias" [Show, Eq, RefinedString]

hoeck : Alias
hoeck = "Stefan Hoeck"

data Weekday =
    Monday
  | Tuesday
  | Wednesday
  | Thursday
  | Friday
  | Saturday
  | Sunday

%runElab derive "Weekday" [Show, Eq, Ord, HDecEq]

Here's a link to a more detailed introduction

Prerequisites

This library uses elab-util. It is therefore recommended to use a package manager such as pack for taking care of your Idris dependencies.