MiniAgda, an experimental language with sized dependent types. Moved to github. (https://github.com/andreasabel/miniagda)
#2Recursion analysis does not work for mutual data
-- 2014-01-09
mutual {
data D -(i : Size) { inn (out : R i) }
data R -(i : Size) { delay (force : [j < i] -> D j) } fields force
}
fun inh : [i : Size] -> R i { inh i .force j = inn (inh j) }
data Empty : Set {}
fun elim : D # -> Empty { elim (inn r) = elim (r .force #) }
-- Stack overflow because MiniAgda thinks D and R are not recursive -- and does eta-expansion into all eternity
- status set to closed
[Thu Jan 9 17:51:46 CET 2014 Andreas Abel <andreas.abel@ifi.lmu.de>; * [ issue 2 ] Recursion analysis for data types now considers all defs in mutual block. Of course, this analysis is over-careful, since a mutual keyword might be spurious. Thus, only use mutual when things are actually mutual!]
How to prevent the removal of line breaksOk, use triple backquote if you want verbatim ``` like this
Or rather like this
here ok?No did not workOr does it have to be 3 lines min?Funny
same lineNew lineOnce more
new lineSeppl
New line after parGetting there, need to leave blank line before ``` to get verbatim paragraphs
Thu Jan 9 17:51:46 CET 2014 Andreas Abel <andreas.abel@ifi.lmu.de> * [ issue 2 ] Recursion analysis for data types now considers all defs in mutual block. Of course, this analysis is over-careful, since a mutual keyword might be spurious. Thus, only use mutual when things are actually mutual!
