MiniAgda, an experimental language with sized dependent types. Moved to github. (https://github.com/andreasabel/miniagda)
#1Coinductive records are also treated as inductive by termination checker.
-- 2014-01-09 -- Treating a type as both inductive and coinductive bears trouble...
data R -(i : Size) { delay (force : [j < i] -> R j) } fields force
-- Coinductive interpretation:
fun inh : [i : Size] -> R i { inh i .force j = inh j }
data Empty : Set {}
-- Inductive interpretation:
fun elim : R # -> Empty { elim (delay r) = elim (r #) }
-- Trouble:
let absurd : Empty = elim (inh #)