# idris2-refined

**Repository Path**: a-alpha/idris2-refined

## Basic Information

- **Project Name**: idris2-refined
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: BSD-3-Clause
- **Default Branch**: main
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2026-02-28
- **Last Updated**: 2026-02-28

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

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

```idris
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](docs/src/Intro.md)

## Prerequisites

This library uses [elab-util](https://github.com/stefan-hoeck/idris2-elab-util).
It is therefore recommended to use a package manager such as
[pack](https://github.com/stefan-hoeck/idris2-pack) for taking care
of your Idris dependencies.

<!-- vi: filetype=idris2:syntax=markdown
-->