All issues

Search results

Universe polymorphism

available-in-voileImplemented in VoileImplemented in Voile

levelsUniverse polymorphismUniverse polymorphism

Status: Open.

#20 In owo-lang/minitt-rs;

· ice1000 opened on Mar 24, 2019

The ability to attach builtin definitions (like Agda BUILTIN pragma

builtins{-# BUILTIN #-}{-# BUILTIN #-}

Status: Open.

#12 In owo-lang/minitt-rs;

· ice1000 opened on Mar 16, 2019

Generalized algebraic data types (indexed inductive families)

gadtsGeneralized algebraic data typesGeneralized algebraic data types

Status: Open.

#11 In owo-lang/minitt-rs;

· ice1000 opened on Mar 16, 2019

Backend framework

backendsCompilationCompilation

Status: Open.

#10 In owo-lang/minitt-rs;

· ice1000 opened on Mar 14, 2019

Termination check (structural induction)

terminationInductionInduction

Status: Open.

#9 In owo-lang/minitt-rs;

· ice1000 opened on Mar 14, 2019

Positivity check for sum types

positivityStrict positiveStrict positive

Status: Open.

#8 In owo-lang/minitt-rs;

· ice1000 opened on Mar 14, 2019

Support "otherwise" in split

available-in-voileImplemented in VoileImplemented in Voile

first-class splitA part of MLPolyRA part of MLPolyR

Status: Open.

#2 In owo-lang/minitt-rs;

· ice1000 opened on Mar 9, 2019

·  

0.3.0