voile 0.1.3

# voile-rs

[![Crates.io](https://img.shields.io/crates/d/voile.svg)][crates]
[![Crates.io](https://img.shields.io/crates/v/voile.svg)][crates]
[![Crates.io](https://img.shields.io/crates/l/voile.svg)][crates]
[![docs.rs](https://docs.rs/voile/badge.svg)][doc-rs]
[![cc-svg]][cc-url]
[![av-svg]][av-url]
[![dep-svg]][dep-rs]

 [crates]: https://crates.io/crates/voile/
 [cc-svg]: https://circleci.com/gh/owo-lang/voile-rs/tree/master.svg?style=svg
 [cc-url]: https://circleci.com/gh/owo-lang/voile-rs/tree/master
 [doc-rs]: https://docs.rs/voile
 [dep-rs]: https://deps.rs/repo/github/owo-lang/voile-rs
 [dep-svg]: https://deps.rs/repo/github/owo-lang/voile-rs/status.svg
 [plugin]: https://github.com/owo-lang/intellij-dtlc/
 [av-url]: https://ci.appveyor.com/project/ice1000/voile-rs/branch/master
 [av-svg]: https://ci.appveyor.com/api/projects/status/8rehm08ncp6whxwt/branch/master?svg=true

Voile is a dependently-typed programming language features in first-class
sums and records.
For language description, please head to the [docs.rs][doc-rs] page.

## Resources

+ [Docs.rs][doc-rs] documentation, including KaTeX-rendered typing rules
+ [Change Log](CHANGELOG.md), useful resource for tracking language evolution
+ [IntelliJ Plugin][plugin], which can export your code as clickable HTML
+ [Code Examples](samples), which also acts as integration test suites

## Install

You can install the voile type-checker by this command
(cargo installation and rust stable toolchain are assumed):

```bash
cargo install voile --bin voilec
```

After installation, you can type-check a voile file by:

```bash
voilec [filename]
```

You can also start a REPL:

```bash
voilec -i
```

## Progress

+ [X] Basic dependent type (minitt-rs things)
+ [X] Universe level support
+ [X] Row-types and kinds
+ [X] Record constructor
+ [X] Record projection
+ [X] Variant constructor
+ [X] Variant eliminator (case-split)