on da79b2c help sign in
Idris-dev
10 folders, 8 files
contribs/vim color adjustment iif/Change TRACE mode to use -O2 lib/Separate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet! papers/Created papers directory rts/Add Proj operator to runtime version of TT Allows extracting arguments without checking constructor first which will make erasing unused values easier shortly samples/Minor parser fixes; added binary sample src/Separate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet! support/Don't build thread support (because it doesn't work...) test/Added simple productivity checker for coinductive definitions Recursive calls must be an argument to a coinductive constructor tutorial/Remove Boehm reference from tutorial .gitignoreNew .gitignore for Cabal's directory and .ibc files. CHANGELOGAdded "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time. LICENSEFix LICENSE MakefileAdded "codata" Constructors of coinductive types evaluate arguments lazily. Corecursive functions do not reduce at compile time. READMEUpdate .cabal and README Setup.hsFirst baby steps towards a new RTS (and towards removing epic dependency) git-credential-osxkeychainerror handling idris.cabalSeparate "productive" and "total" in totality checker Productive can call Total, but not vice versa. This is still a temporary solution - don't rely on anything yet!