auxolotl/docs
26
0
Fork 1
mirror of https://git.gay/pyrox/aux-docs synced 2024-11-23 14:17:57 +00:00
Code Issues Packages Projects Releases Wiki Activity
docs/Nixpkgs/Languages-And-Frameworks/idris2.section/index.html

2700 lines
50 KiB
HTML
Raw Blame History

<!doctype html>
<html lang="en" class="no-js">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width,initial-scale=1">
<meta name="description" content="Aux Documentation">
<meta name="author" content="Nixpkgs Aux, and Lix Contributors">
<link rel="canonical" href="https://docs.auxolotl.org/Nixpkgs/Languages-And-Frameworks/idris2.section/">
<link rel="prev" href="../idris.section/">
<link rel="next" href="../ios.section/">
<link rel="icon" href="../../../assets/aux-logo.svg">
<meta name="generator" content="mkdocs-1.6.0, mkdocs-material-9.5.29">
<title>Idris2 - Aux Docs</title>
<link rel="stylesheet" href="../../../assets/stylesheets/main.76a95c52.min.css">
<link rel="stylesheet" href="../../../assets/stylesheets/palette.06af60db.min.css">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link rel="stylesheet" href="https://fonts.bunny.net/css?family=IBM+Plex+Sans:300,300i,400,400i,700,700i%7CIBM+Plex+Mono:400,400i,700,700i&display=fallback">
<style>:root{--md-text-font:"IBM Plex Sans";--md-code-font:"IBM Plex Mono"}</style>
<script>__md_scope=new URL("../../..",location),__md_hash=e=>[...e].reduce((e,_)=>(e<<5)-e+_.charCodeAt(0),0),__md_get=(e,_=localStorage,t=__md_scope)=>JSON.parse(_.getItem(t.pathname+"."+e)),__md_set=(e,_,t=localStorage,a=__md_scope)=>{try{t.setItem(a.pathname+"."+e,JSON.stringify(_))}catch(e){}}</script>
<meta property="og:type" content="website" >
<meta property="og:title" content="Idris2 {#sec-idris2} - Aux Docs" >
<meta property="og:description" content="Aux Documentation" >
<meta property="og:image" content="https://docs.auxolotl.org/assets/images/social/Nixpkgs/Languages-And-Frameworks/idris2.section.png" >
<meta property="og:image:type" content="image/png" >
<meta property="og:image:width" content="1200" >
<meta property="og:image:height" content="630" >
<meta property="og:url" content="https://docs.auxolotl.org/Nixpkgs/Languages-And-Frameworks/idris2.section/" >
<meta name="twitter:card" content="summary_large_image" >
<meta name="twitter:title" content="Idris2 {#sec-idris2} - Aux Docs" >
<meta name="twitter:description" content="Aux Documentation" >
<meta name="twitter:image" content="https://docs.auxolotl.org/assets/images/social/Nixpkgs/Languages-And-Frameworks/idris2.section.png" >
</head>
<body dir="ltr" data-md-color-scheme="default" data-md-color-primary="indigo" data-md-color-accent="blue">
<input class="md-toggle" data-md-toggle="drawer" type="checkbox" id="__drawer" autocomplete="off">
<input class="md-toggle" data-md-toggle="search" type="checkbox" id="__search" autocomplete="off">
<label class="md-overlay" for="__drawer"></label>
<div data-md-component="skip">
<a href="#sec-idris2" class="md-skip">
Skip to content
</a>
</div>
<div data-md-component="announce">
</div>
<header class="md-header" data-md-component="header">
<nav class="md-header__inner md-grid" aria-label="Header">
<a href="../../.." title="Aux Docs" class="md-header__button md-logo" aria-label="Aux Docs" data-md-component="logo">
<img src="../../../assets/aux-logo.svg" alt="logo">
</a>
<label class="md-header__button md-icon" for="__drawer">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M3 6h18v2H3V6m0 5h18v2H3v-2m0 5h18v2H3v-2Z"/></svg>
</label>
<div class="md-header__title" data-md-component="header-title">
<div class="md-header__ellipsis">
<div class="md-header__topic">
<span class="md-ellipsis">
Aux Docs
</span>
</div>
<div class="md-header__topic" data-md-component="header-topic">
<span class="md-ellipsis">
Idris2
</span>
</div>
</div>
</div>
<form class="md-header__option" data-md-component="palette">
<input class="md-option" data-md-color-media="(prefers-color-scheme: light)" data-md-color-scheme="default" data-md-color-primary="indigo" data-md-color-accent="blue" aria-label="Dark Mode" type="radio" name="__palette" id="__palette_0">
<label class="md-header__button md-icon" title="Dark Mode" for="__palette_1" hidden>
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="m17.75 4.09-2.53 1.94.91 3.06-2.63-1.81-2.63 1.81.91-3.06-2.53-1.94L12.44 4l1.06-3 1.06 3 3.19.09m3.5 6.91-1.64 1.25.59 1.98-1.7-1.17-1.7 1.17.59-1.98L15.75 11l2.06-.05L18.5 9l.69 1.95 2.06.05m-2.28 4.95c.83-.08 1.72 1.1 1.19 1.85-.32.45-.66.87-1.08 1.27C15.17 23 8.84 23 4.94 19.07c-3.91-3.9-3.91-10.24 0-14.14.4-.4.82-.76 1.27-1.08.75-.53 1.93.36 1.85 1.19-.27 2.86.69 5.83 2.89 8.02a9.96 9.96 0 0 0 8.02 2.89m-1.64 2.02a12.08 12.08 0 0 1-7.8-3.47c-2.17-2.19-3.33-5-3.49-7.82-2.81 3.14-2.7 7.96.31 10.98 3.02 3.01 7.84 3.12 10.98.31Z"/></svg>
</label>
<input class="md-option" data-md-color-media="(prefers-color-scheme: dark)" data-md-color-scheme="slate" data-md-color-primary="indigo" data-md-color-accent="blue" aria-label="Light Mode" type="radio" name="__palette" id="__palette_1">
<label class="md-header__button md-icon" title="Light Mode" for="__palette_0" hidden>
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12 7a5 5 0 0 1 5 5 5 5 0 0 1-5 5 5 5 0 0 1-5-5 5 5 0 0 1 5-5m0 2a3 3 0 0 0-3 3 3 3 0 0 0 3 3 3 3 0 0 0 3-3 3 3 0 0 0-3-3m0-7 2.39 3.42C13.65 5.15 12.84 5 12 5c-.84 0-1.65.15-2.39.42L12 2M3.34 7l4.16-.35A7.2 7.2 0 0 0 5.94 8.5c-.44.74-.69 1.5-.83 2.29L3.34 7m.02 10 1.76-3.77a7.131 7.131 0 0 0 2.38 4.14L3.36 17M20.65 7l-1.77 3.79a7.023 7.023 0 0 0-2.38-4.15l4.15.36m-.01 10-4.14.36c.59-.51 1.12-1.14 1.54-1.86.42-.73.69-1.5.83-2.29L20.64 17M12 22l-2.41-3.44c.74.27 1.55.44 2.41.44.82 0 1.63-.17 2.37-.44L12 22Z"/></svg>
</label>
</form>
<script>var media,input,key,value,palette=__md_get("__palette");if(palette&&palette.color){"(prefers-color-scheme)"===palette.color.media&&(media=matchMedia("(prefers-color-scheme: light)"),input=document.querySelector(media.matches?"[data-md-color-media='(prefers-color-scheme: light)']":"[data-md-color-media='(prefers-color-scheme: dark)']"),palette.color.media=input.getAttribute("data-md-color-media"),palette.color.scheme=input.getAttribute("data-md-color-scheme"),palette.color.primary=input.getAttribute("data-md-color-primary"),palette.color.accent=input.getAttribute("data-md-color-accent"));for([key,value]of Object.entries(palette.color))document.body.setAttribute("data-md-color-"+key,value)}</script>
<label class="md-header__button md-icon" for="__search">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0 1 16 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 0 1 9.5 16 6.5 6.5 0 0 1 3 9.5 6.5 6.5 0 0 1 9.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5Z"/></svg>
</label>
<div class="md-search" data-md-component="search" role="dialog">
<label class="md-search__overlay" for="__search"></label>
<div class="md-search__inner" role="search">
<form class="md-search__form" name="search">
<input type="text" class="md-search__input" name="query" aria-label="Search" placeholder="Search" autocapitalize="off" autocorrect="off" autocomplete="off" spellcheck="false" data-md-component="search-query" required>
<label class="md-search__icon md-icon" for="__search">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M9.5 3A6.5 6.5 0 0 1 16 9.5c0 1.61-.59 3.09-1.56 4.23l.27.27h.79l5 5-1.5 1.5-5-5v-.79l-.27-.27A6.516 6.516 0 0 1 9.5 16 6.5 6.5 0 0 1 3 9.5 6.5 6.5 0 0 1 9.5 3m0 2C7 5 5 7 5 9.5S7 14 9.5 14 14 12 14 9.5 12 5 9.5 5Z"/></svg>
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M20 11v2H8l5.5 5.5-1.42 1.42L4.16 12l7.92-7.92L13.5 5.5 8 11h12Z"/></svg>
</label>
<nav class="md-search__options" aria-label="Search">
<button type="reset" class="md-search__icon md-icon" title="Clear" aria-label="Clear" tabindex="-1">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M19 6.41 17.59 5 12 10.59 6.41 5 5 6.41 10.59 12 5 17.59 6.41 19 12 13.41 17.59 19 19 17.59 13.41 12 19 6.41Z"/></svg>
</button>
</nav>
</form>
<div class="md-search__output">
<div class="md-search__scrollwrap" tabindex="0" data-md-scrollfix>
<div class="md-search-result" data-md-component="search-result">
<div class="md-search-result__meta">
Initializing search
</div>
<ol class="md-search-result__list" role="presentation"></ol>
</div>
</div>
</div>
</div>
</div>
<div class="md-header__source">
<a href="https://git.auxolotl.org/auxolotl/docs" title="Go to repository" class="md-source" data-md-component="source">
<div class="md-source__icon md-icon">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
</div>
<div class="md-source__repository">
auxolotl/docs
</div>
</a>
</div>
</nav>
</header>
<div class="md-container" data-md-component="container">
<nav class="md-tabs" aria-label="Tabs" data-md-component="tabs">
<div class="md-grid">
<ul class="md-tabs__list">
<li class="md-tabs__item">
<a href="../../.." class="md-tabs__link">
Aux Documentation Hub
</a>
</li>
<li class="md-tabs__item">
<a href="../../../TODO/" class="md-tabs__link">
TODO
</a>
</li>
<li class="md-tabs__item">
<a href="../../../Aux/" class="md-tabs__link">
Aux
</a>
</li>
<li class="md-tabs__item">
<a href="../../../Lix/" class="md-tabs__link">
Lix
</a>
</li>
<li class="md-tabs__item">
<a href="../../../NixOS/appstream/" class="md-tabs__link">
NixOS
</a>
</li>
<li class="md-tabs__item md-tabs__item--active">
<a href="../../" class="md-tabs__link">
Nixpkgs
</a>
</li>
</ul>
</div>
</nav>
<main class="md-main" data-md-component="main">
<div class="md-main__inner md-grid">
<div class="md-sidebar md-sidebar--primary" data-md-component="sidebar" data-md-type="navigation" >
<div class="md-sidebar__scrollwrap">
<div class="md-sidebar__inner">
<nav class="md-nav md-nav--primary md-nav--lifted" aria-label="Navigation" data-md-level="0">
<label class="md-nav__title" for="__drawer">
<a href="../../.." title="Aux Docs" class="md-nav__button md-logo" aria-label="Aux Docs" data-md-component="logo">
<img src="../../../assets/aux-logo.svg" alt="logo">
</a>
Aux Docs
</label>
<div class="md-nav__source">
<a href="https://git.auxolotl.org/auxolotl/docs" title="Go to repository" class="md-source" data-md-component="source">
<div class="md-source__icon md-icon">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
</div>
<div class="md-source__repository">
auxolotl/docs
</div>
</a>
</div>
<ul class="md-nav__list" data-md-scrollfix>
<li class="md-nav__item">
<a href="../../.." class="md-nav__link">
<span class="md-ellipsis">
Aux Documentation Hub
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../../../TODO/" class="md-nav__link">
<span class="md-ellipsis">
TODO
</span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../../Aux/" class="md-nav__link">
<span class="md-ellipsis">
Aux
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../../Lix/" class="md-nav__link">
<span class="md-ellipsis">
Lix
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../../NixOS/appstream/" class="md-nav__link">
<span class="md-ellipsis">
NixOS
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--active md-nav__item--section md-nav__item--nested">
<input class="md-nav__toggle md-toggle " type="checkbox" id="__nav_6" checked>
<div class="md-nav__link md-nav__container">
<a href="../../" class="md-nav__link ">
<span class="md-ellipsis">
Nixpkgs
</span>
</a>
<label class="md-nav__link " for="__nav_6" id="__nav_6_label" tabindex="">
<span class="md-nav__icon md-icon"></span>
</label>
</div>
<nav class="md-nav" data-md-level="1" aria-labelledby="__nav_6_label" aria-expanded="true">
<label class="md-nav__title" for="__nav_6">
<span class="md-nav__icon md-icon"></span>
Nixpkgs
</label>
<ul class="md-nav__list" data-md-scrollfix>
<li class="md-nav__item">
<a href="../../options/" class="md-nav__link">
<span class="md-ellipsis">
Options
</span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Build-Helpers/" class="md-nav__link">
<span class="md-ellipsis">
Build Helpers
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Development/" class="md-nav__link">
<span class="md-ellipsis">
Development
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Functions/" class="md-nav__link">
<span class="md-ellipsis">
Functions
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Hooks/" class="md-nav__link">
<span class="md-ellipsis">
Hooks
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--active md-nav__item--nested">
<input class="md-nav__toggle md-toggle " type="checkbox" id="__nav_6_7" checked>
<div class="md-nav__link md-nav__container">
<a href="../" class="md-nav__link ">
<span class="md-ellipsis">
Languages And Frameworks
</span>
</a>
<label class="md-nav__link " for="__nav_6_7" id="__nav_6_7_label" tabindex="0">
<span class="md-nav__icon md-icon"></span>
</label>
</div>
<nav class="md-nav" data-md-level="2" aria-labelledby="__nav_6_7_label" aria-expanded="true">
<label class="md-nav__title" for="__nav_6_7">
<span class="md-nav__icon md-icon"></span>
Languages And Frameworks
</label>
<ul class="md-nav__list" data-md-scrollfix>
<li class="md-nav__item">
<a href="../agda.section/" class="md-nav__link">
<span class="md-ellipsis">
Agda
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../android.section/" class="md-nav__link">
<span class="md-ellipsis">
Android
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../beam.section/" class="md-nav__link">
<span class="md-ellipsis">
BEAM Languages (Erlang, Elixir &amp; LFE)
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../bower.section/" class="md-nav__link">
<span class="md-ellipsis">
Bower
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../chicken.section/" class="md-nav__link">
<span class="md-ellipsis">
CHICKEN
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../coq.section/" class="md-nav__link">
<span class="md-ellipsis">
Coq and coq packages
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../crystal.section/" class="md-nav__link">
<span class="md-ellipsis">
Crystal
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../cuda.section/" class="md-nav__link">
<span class="md-ellipsis">
CUDA
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../cuelang.section/" class="md-nav__link">
<span class="md-ellipsis">
Cue (Cuelang)
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../dart.section/" class="md-nav__link">
<span class="md-ellipsis">
Dart
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../dhall.section/" class="md-nav__link">
<span class="md-ellipsis">
Dhall
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../dlang.section/" class="md-nav__link">
<span class="md-ellipsis">
D (Dlang)
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../dotnet.section/" class="md-nav__link">
<span class="md-ellipsis">
Dotnet
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../emscripten.section/" class="md-nav__link">
<span class="md-ellipsis">
Emscripten
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../gnome.section/" class="md-nav__link">
<span class="md-ellipsis">
GNOME
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../go.section/" class="md-nav__link">
<span class="md-ellipsis">
Go
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../gradle.section/" class="md-nav__link">
<span class="md-ellipsis">
Gradle
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../hare.section/" class="md-nav__link">
<span class="md-ellipsis">
Hare
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../haskell.section/" class="md-nav__link">
<span class="md-ellipsis">
Haskell
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../hy.section/" class="md-nav__link">
<span class="md-ellipsis">
Hy
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../idris.section/" class="md-nav__link">
<span class="md-ellipsis">
Idris
</span>
</a>
</li>
<li class="md-nav__item md-nav__item--active">
<input class="md-nav__toggle md-toggle" type="checkbox" id="__toc">
<a href="./" class="md-nav__link md-nav__link--active">
<span class="md-ellipsis">
Idris2
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../ios.section/" class="md-nav__link">
<span class="md-ellipsis">
iOS
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../java.section/" class="md-nav__link">
<span class="md-ellipsis">
Java
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../javascript.section/" class="md-nav__link">
<span class="md-ellipsis">
Javascript
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../julia.section/" class="md-nav__link">
<span class="md-ellipsis">
Julia
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../lisp.section/" class="md-nav__link">
<span class="md-ellipsis">
lisp-modules
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../lua.section/" class="md-nav__link">
<span class="md-ellipsis">
Lua
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../maven.section/" class="md-nav__link">
<span class="md-ellipsis">
Maven
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../nim.section/" class="md-nav__link">
<span class="md-ellipsis">
Nim
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../ocaml.section/" class="md-nav__link">
<span class="md-ellipsis">
OCaml
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../octave.section/" class="md-nav__link">
<span class="md-ellipsis">
Octave
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../perl.section/" class="md-nav__link">
<span class="md-ellipsis">
Perl
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../php.section/" class="md-nav__link">
<span class="md-ellipsis">
PHP
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../pkg-config.section/" class="md-nav__link">
<span class="md-ellipsis">
pkg-config
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../python.section/" class="md-nav__link">
<span class="md-ellipsis">
Python
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../qt.section/" class="md-nav__link">
<span class="md-ellipsis">
Qt
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../r.section/" class="md-nav__link">
<span class="md-ellipsis">
R
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../ruby.section/" class="md-nav__link">
<span class="md-ellipsis">
Ruby
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../rust.section/" class="md-nav__link">
<span class="md-ellipsis">
Rust
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../scheme.section/" class="md-nav__link">
<span class="md-ellipsis">
Scheme
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../swift.section/" class="md-nav__link">
<span class="md-ellipsis">
Swift
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../texlive.section/" class="md-nav__link">
<span class="md-ellipsis">
TeX Live
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../titanium.section/" class="md-nav__link">
<span class="md-ellipsis">
Titanium
</span>
</a>
</li>
<li class="md-nav__item">
<a href="../vim.section/" class="md-nav__link">
<span class="md-ellipsis">
Vim
</span>
</a>
</li>
</ul>
</nav>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Library-Reference/asserts/" class="md-nav__link">
<span class="md-ellipsis">
Library Reference
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Module-System/module-system.chapter/" class="md-nav__link">
<span class="md-ellipsis">
Module System
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Packages/" class="md-nav__link">
<span class="md-ellipsis">
Packages
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Standard-Environment/" class="md-nav__link">
<span class="md-ellipsis">
Standard Environment
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
<li class="md-nav__item md-nav__item--pruned md-nav__item--nested">
<a href="../../Using-Nixpkgs/" class="md-nav__link">
<span class="md-ellipsis">
Using Nixpkgs
</span>
<span class="md-nav__icon md-icon"></span>
</a>
</li>
</ul>
</nav>
</li>
</ul>
</nav>
</div>
</div>
</div>
<div class="md-sidebar md-sidebar--secondary" data-md-component="sidebar" data-md-type="toc" >
<div class="md-sidebar__scrollwrap">
<div class="md-sidebar__inner">
<nav class="md-nav md-nav--secondary" aria-label="Table of contents">
</nav>
</div>
</div>
</div>
<div class="md-content" data-md-component="content">
<article class="md-content__inner md-typeset">
<h1 id="sec-idris2">Idris2</h1>
<p>In addition to exposing the Idris2 compiler itself, Nixpkgs exposes an <code>idris2Packages.buildIdris</code> helper to make it a bit more ergonomic to build Idris2 executables or libraries.</p>
<p>The <code>buildIdris</code> function takes an attribute set that defines at a minimum the <code>src</code> and <code>ipkgName</code> of the package to be built and any <code>idrisLibraries</code> required to build it. The <code>src</code> is the same source you're familiar with and the <code>ipkgName</code> must be the name of the <code>ipkg</code> file for the project (omitting the <code>.ipkg</code> extension). The <code>idrisLibraries</code> is a list of other library derivations created with <code>buildIdris</code>. You can optionally specify other derivation properties as needed but sensible defaults for <code>configurePhase</code>, <code>buildPhase</code>, and <code>installPhase</code> are provided.</p>
<p>Importantly, <code>buildIdris</code> does not create a single derivation but rather an attribute set with two properties: <code>executable</code> and <code>library</code>. The <code>executable</code> property is a derivation and the <code>library</code> property is a function that will return a derivation for the library with or without source code included. Source code need not be included unless you are aiming to use IDE or LSP features that are able to jump to definitions within an editor.</p>
<p>A simple example of a fully packaged library would be the <a href="https://github.com/idris-community/LSP-lib"><code>LSP-lib</code></a> found in the <code>idris-community</code> GitHub organization.
<div class="highlight"><pre><span></span><code><span class="p">{</span> fetchFromGitHub<span class="p">,</span> idris2Packages <span class="p">}:</span>
<span class="k">let</span> <span class="ss">lspLibPkg</span> <span class="o">=</span> idris2Packages<span class="o">.</span>buildIdris <span class="p">{</span>
<span class="ss">ipkgName</span> <span class="o">=</span> <span class="s2">&quot;lsp-lib&quot;</span><span class="p">;</span>
<span class="ss">src</span> <span class="o">=</span> fetchFromGitHub <span class="p">{</span>
<span class="ss">owner</span> <span class="o">=</span> <span class="s2">&quot;idris-community&quot;</span><span class="p">;</span>
<span class="ss">repo</span> <span class="o">=</span> <span class="s2">&quot;LSP-lib&quot;</span><span class="p">;</span>
<span class="ss">rev</span> <span class="o">=</span> <span class="s2">&quot;main&quot;</span><span class="p">;</span>
<span class="ss">hash</span> <span class="o">=</span> <span class="s2">&quot;sha256-EvSyMCVyiy9jDZMkXQmtwwMoLaem1GsKVFqSGNNHHmY=&quot;</span><span class="p">;</span>
<span class="p">};</span>
<span class="ss">idrisLibraries</span> <span class="o">=</span> <span class="p">[</span> <span class="p">];</span>
<span class="p">};</span>
<span class="k">in</span> lspLibPkg<span class="o">.</span>library <span class="p">{</span> <span class="ss">withSource</span> <span class="o">=</span> <span class="no">true</span><span class="p">;</span> <span class="p">}</span>
</code></pre></div></p>
<p>The above results in a derivation with the installed library results (with sourcecode).</p>
<p>A slightly more involved example of a fully packaged executable would be the <a href="https://github.com/idris-community/idris2-lsp"><code>idris2-lsp</code></a> which is an Idris2 language server that uses the <code>LSP-lib</code> found above.
<div class="highlight"><pre><span></span><code><span class="p">{</span> callPackage<span class="p">,</span> fetchFromGitHub<span class="p">,</span> idris2Packages <span class="p">}:</span> <span class="s2">&quot;Assuming the previous example lives in `lsp-lib.nix`:</span>
<span class="s2">let lspLib = callPackage ./lsp-lib.nix { };</span>
<span class="s2"> inherit (idris2Packages) idris2Api;</span>
<span class="s2"> lspPkg = idris2Packages.buildIdris {</span>
<span class="s2"> ipkgName = &quot;</span>idris2-lsp<span class="s2">&quot;;</span>
<span class="s2"> src = fetchFromGitHub {</span>
<span class="s2"> owner = &quot;</span>idris-community<span class="s2">&quot;;</span>
<span class="s2"> repo = &quot;</span>idris2-lsp<span class="s2">&quot;;</span>
<span class="s2"> rev = &quot;</span>main<span class="s2">&quot;;</span>
<span class="s2"> hash = &quot;</span>sha256-vQTzEltkx7uelDtXOHc6QRWZ4cSlhhm5ziOqWA<span class="o">+</span><span class="ss">aujk</span><span class="o">=</span><span class="s2">&quot;;</span>
<span class="s2"> };</span>
<span class="s2"> idrisLibraries = [idris2Api lspLib];</span>
<span class="s2"> };</span>
<span class="s2">in lspPkg.executable</span>
</code></pre></div></p>
<p>The above uses the default value of <code>withSource = false</code> for the <code>idris2Api</code> but could be modified to include that library's source by passing <code>(idris2Api { withSource = true; })</code> to <code>idrisLibraries</code> instead. <code>idris2Api</code> in the above derivation comes built in with <code>idris2Packages</code>. This library exposes many of the otherwise internal APIs of the Idris2 compiler.</p>
</article>
</div>
<script>var target=document.getElementById(location.hash.slice(1));target&&target.name&&(target.checked=target.name.startsWith("__tabbed_"))</script>
</div>
</main>
<footer class="md-footer">
<div class="md-footer-meta md-typeset">
<div class="md-footer-meta__inner md-grid">
<div class="md-copyright">
<div class="md-copyright__highlight">
Licenced MIT
</div>
Made with
<a href="https://squidfunk.github.io/mkdocs-material/" target="_blank" rel="noopener">
Material for MkDocs
</a>
</div>
<div class="md-social">
<a href="https://git.auxolotl.org/auxolotl/docs" target="_blank" rel="noopener" title="Aux Docs Repo" class="md-social__link">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M16.777 0a2.9 2.9 0 1 1-2.529 4.322H12.91a4.266 4.266 0 0 0-4.265 4.195v2.118a7.076 7.076 0 0 1 4.147-1.42l.118-.002h1.338a2.9 2.9 0 0 1 5.43 1.422 2.9 2.9 0 0 1-5.43 1.422H12.91a4.266 4.266 0 0 0-4.265 4.195v2.319A2.9 2.9 0 0 1 7.222 24 2.9 2.9 0 0 1 5.8 18.57V8.589a7.109 7.109 0 0 1 6.991-7.108l.118-.001h1.338A2.9 2.9 0 0 1 16.778 0ZM7.223 19.905a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Zm9.554-10.464a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.39Zm0-7.735a1.194 1.194 0 1 0 0 2.389 1.194 1.194 0 0 0 0-2.389Z"/></svg>
</a>
<a href="https://forum.aux.computer/" target="_blank" rel="noopener" title="Aux Forum" class="md-social__link">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M12.103 0C18.666 0 24 5.485 24 11.997c0 6.51-5.33 11.99-11.9 11.99L0 24V11.79C0 5.28 5.532 0 12.103 0zm.116 4.563a7.395 7.395 0 0 0-6.337 3.57 7.247 7.247 0 0 0-.148 7.22L4.4 19.61l4.794-1.074a7.424 7.424 0 0 0 8.136-1.39 7.256 7.256 0 0 0 1.737-7.997 7.375 7.375 0 0 0-6.84-4.585h-.008z"/></svg>
</a>
<a href="https://wiki.auxolotl.org/" target="_blank" rel="noopener" title="Aux Wiki" class="md-social__link">
<svg xmlns="http://www.w3.org/2000/svg" viewBox="0 0 24 24"><path d="M17.801 13.557c.148.098.288.202.417.313 1.854 1.6 3.127 4.656 2.582 7.311-1.091-.255-5.747-1.055-7.638-3.383-.91-1.12-1.366-2.081-1.569-2.885a5.65 5.65 0 0 0 .034-.219c.089.198.197.35.313.466.24.24.521.335.766.372.304.046.594-.006.806-.068l.001.001c.05-.015.433-.116.86-.342.325-.173 2.008-.931 3.428-1.566Zm-7.384 1.435C9.156 16.597 6.6 18.939.614 18.417c.219-1.492 1.31-3.019 2.51-4.11.379-.345.906-.692 1.506-1.009.286.168.598.332.939.486 2.689 1.221 3.903 1.001 4.89.573a1.3 1.3 0 0 0 .054-.025 6.156 6.156 0 0 0-.096.66Zm4.152-.462c.38-.341.877-.916 1.383-1.559-.389-.15-.866-.371-1.319-.591-.598-.29-1.305-.283-2.073-.315a4.685 4.685 0 0 1-.804-.103c.014-.123.027-.246.038-.369.062.104.673.057.871.057.354 0 1.621.034 3.074-.574 1.452-.608 2.55-1.706 3.022-3.225.474-1.52.22-3.091-.168-3.952-.169.709-1.453 2.381-1.926 2.871-.473.489-2.381 2.296-2.972 2.921-.7.74-.688.793-1.332 1.302-.202.19-.499.402-.563.53.027-.338.039-.675.027-.997a7.653 7.653 0 0 0-.032-.523c.322-.059.567-.522.567-.861 0-.224-.106-.247-.271-.229.075-.894.382-3.923 1.254-4.281.218.109.831.068.649-.295-.182-.364-.825-.074-1.081.266-.28.374-.956 2.046-.92 4.324-.113.014-.174.033-.322.033-.171 0-.321-.04-.433-.05.034-2.275-.714-3.772-.84-4.169-.12-.375-.491-.596-.781-.596-.146 0-.272.056-.333.179-.182.363.459.417.677.308.706.321 1.156 3.519 1.254 4.277-.125-.006-.199.035-.199.233 0 .311.17.756.452.843a.442.442 0 0 0-.007.03s-.287.99-.413 2.189a4.665 4.665 0 0 1-.718-.225c-.714-.286-1.355-.583-2.019-.566-.664.018-1.366.023-1.804-.036-.438-.058-.649-.15-.649-.15s-.234.365.257 1.075c.42.607 1.055 1.047 1.644 1.18.589.134 1.972.18 2.785-.377.16-.109.317-.228.459-.34a8.717 8.717 0 0 0-.013.626c-.289.753-.571 1.993-.268 3.338 0-.001.701-.842.787-2.958.006-.144.009-.271.01-.383.052-.248.103-.518.148-.799.072.135.151.277.234.413.511.842 1.791 1.37 2.383 1.49.091.019.187.032.285.038Zm-1.12.745c-.188.055-.445.1-.713.059-.21-.031-.45-.11-.655-.316-.169-.168-.312-.419-.401-.789a9.837 9.837 0 0 0 .039-.82l.049-.243c.563.855 1.865 1.398 2.476 1.522.036.008.072.014.109.02l-.013.009c-.579.415-.76.503-.891.558Zm6.333-2.818c-.257.114-4.111 1.822-5.246 2.363.98-.775 3.017-3.59 3.699-4.774 1.062.661 1.468 1.109 1.623 1.441.101.217.09.38.096.515a.57.57 0 0 1-.172.455Zm-9.213 1.62a1.606 1.606 0 0 1-.19.096c-.954.414-2.126.61-4.728-.571-2.023-.918-3.024-2.157-3.371-2.666.476.161 1.471.473 2.157.524.282.021.703.068 1.167.125.021.209.109.486.345.829l.001.001c.451.651 1.134 1.119 1.765 1.262.622.141 2.083.182 2.942-.407a3.12 3.12 0 0 0 .132-.093l.001.179a6.052 6.052 0 0 0-.221.721Zm5.512-1.271a17.49 17.49 0 0 1-1.326-.589c.437.042 1.054.083 1.692.108-.121.162-.244.323-.366.481Zm.932-1.26c-.12.17-.245.343-.373.517-.241.018-.478.03-.709.038a29.05 29.05 0 0 1-.741-.048c.608-.065 1.228-.252 1.823-.507Zm.22-.315c-.809.382-1.679.648-2.507.648-.472 0-.833.018-1.139.039v.001c-.324-.031-.665-.039-1.019-.054a3.555 3.555 0 0 1-.152-.009c.102-.002.192-.006.249-.006.363 0 1.662.034 3.151-.589 1.508-.632 2.645-1.773 3.136-3.351.37-1.186.31-2.402.086-3.312.458-.336.86-.651 1.147-.91.501-.451.743-.733.848-.869.199.206.714.864.685 2.138-.036 1.611-.606 3.187-1.501 4.154a9.099 9.099 0 0 1-1.321 1.132 11.978 11.978 0 0 0-.644-.422l-.089-.055-.051.091c-.184.332-.5.825-.879 1.374ZM4.763 5.817c-.157 1.144.113 2.323.652 3.099.539.776 2.088 2.29 3.614 2.505.991.14 2.055.134 2.055.134s-.593-.576-1.114-1.66c-.521-1.085-.948-2.104-1.734-2.786-.785-.681-1.601-1.416-2.045-1.945-.444-.53-.59-.86-.59-.86s-.656.175-.838 1.513Zm14.301 4.549a9.162 9.162 0 0 0 1.3-1.12c.326-.352.611-.782.845-1.265 1.315.145 2.399.371 2.791.434 0 0-.679 1.971-3.945 3.022l-.016-.035c-.121-.26-.385-.594-.975-1.036Zm-11.634.859a8.537 8.537 0 0 1-.598-.224c-1.657-.693-2.91-1.944-3.449-3.678-.498-1.601-.292-3.251.091-4.269.225.544.758 1.34 1.262 2.01a3.58 3.58 0 0 0-.172.726c-.163 1.197.123 2.428.687 3.24.416.599 1.417 1.62 2.555 2.193-.128.002-.253.003-.376.002Zm-1.758-.077c-.958-.341-1.901-.787-2.697-1.368C-.07 7.559 0 6.827 0 6.827s1.558-.005 3.088.179c.03.126.065.251.104.377.557 1.791 1.851 3.086 3.562 3.803l.047.019a4.254 4.254 0 0 1-.267-.026h-.001c-.401-.053-.595-.135-.595-.135l-.157-.069-.092.144-.017.029Zm6.807-1.59c.086.017.136.058.136.145 0 .197-.242.5-.597.597l-.01-.161a.887.887 0 0 0 .283-.243c.078-.099.142-.217.188-.338Zm-1.591.006c.033.1.076.197.129.282.061.097.134.18.217.24l-.021.083c-.276-.093-.424-.293-.424-.466 0-.078.035-.119.099-.139Zm-.025-.664c-.275-.816-.795-2.022-1.505-2.179-.296.072-.938.096-.691-.145.246-.24 1.085-.048 1.283.217.145.194.744.806 1.011 1.737l.032.227a.324.324 0 0 0-.13.143Zm1.454-.266c.251-.99.889-1.639 1.039-1.841.197-.265 1.036-.457 1.283-.217.247.241-.395.217-.691.145-.69.152-1.2 1.296-1.481 2.109a.364.364 0 0 0-.067-.059.37.37 0 0 0-.092-.043l.009-.094Zm4.802-2.708a9.875 9.875 0 0 1-.596.705c-.304.315-1.203 1.176-1.963 1.916.647-.955 1.303-1.806 2.184-2.376.123-.08.249-.161.375-.245Z"/></svg>
</a>
</div>
</div>
</div>
</footer>
</div>
<div class="md-dialog" data-md-component="dialog">
<div class="md-dialog__inner md-typeset"></div>
</div>
<script id="__config" type="application/json">{"base": "../../..", "features": ["content.tooltips", "search.highlight", "navigation.tabs", "navigation.indexes", "navigation.prune"], "search": "../../../assets/javascripts/workers/search.b8dbb3d2.min.js", "translations": {"clipboard.copied": "Copied to clipboard", "clipboard.copy": "Copy to clipboard", "search.result.more.one": "1 more on this page", "search.result.more.other": "# more on this page", "search.result.none": "No matching documents", "search.result.one": "1 matching document", "search.result.other": "# matching documents", "search.result.placeholder": "Type to start searching", "search.result.term.missing": "Missing", "select.version": "Select version"}}</script>
<script src="../../../assets/javascripts/bundle.fe8b6f2b.min.js"></script>
</body>
</html>
Reference in a new issue View git blame Copy permalink