|Tags||c llvm programming-language functional haskell ml agda|
0.1227 Mar 2016 03:15 minor feature: : Improved startup performance by reducing the processing of an already imported. Module that has changed accessibility.
0.1101 Feb 2016 03:15 minor feature: : Updated export rules. The export rules are: - 'private' means that the definition is not exported at all. - 'export' means that the top level type is exported, but not the definition. In the case of 'data', this means the type constructor is exported but not the data constructors. - 'public export' means that the entire definition is exported. By default, names are 'private'. This can be altered with an access directive as before. Exported types can only refer to other exported names. Publicly exported definitions can only refer to publicly exported names. Minor language changes. The ' static ' annotation is changed to ' static' to be consistent with the. other annotations.
0.10.129 Jan 2016 03:15 minor feature: : The ' static ' annotation is changed to ' static' to be consistent with the. Other annotations.
0.1021 Jan 2016 06:25 minor feature: : 'class' and 'instance' are now deprecated keywords. They have been. Replaced by 'interface' and 'implementation' respectively. This is to Properly reflect their purpose. (/) operator moved into new Fractional interface. Idris' logging infrastructure has been categorised. Command line and repl. Are available. For command line the option `--logging-categories CATS` is used to pass in the categories. Here `CATS` is a colon separated quoted. String containing the categories to log. The REPL command is `logcats CATS`. Where `CATS` is a whitespace separated list of categoriese. Default is for. All categories to be logged. New flag `--listlogcats` to list logging categories.`.
0.9.2120 Dec 2015 03:15 minor documentation: : Idris' logging infrastructure has been categorised. Command line and repl. Are available. For command line the option `--logging-categories CATS` is used to pass in the categories. Here `CATS` is a colon separated quoted. String containing the categories to log. The REPL command is `logcats CATS`. Where `CATS` is a whitespace separated list of categoriese. Default is for. All categories to be logged.
0.9.2002 Sep 2015 07:05 minor documentation: : Language updates. None so far . Library updates. None so far . Tool updates. None so far . Miscellaneous updates. None so far .
0.9.1925 May 2015 03:15 minor feature: : The Show class has been moved into Prelude.Show and augmented with the method showPrec, which allows correct parenthesization of showed terms. This comes with the type Prec of precedences and a few helper functions.
0.9.1824 Mar 2015 03:15 minor feature: : --------------. Syntax rules no longer perform variable capture. Users of effects will need to explicitly name results in dependent effect signatures instead of using the default name "result".
0.9.1713 Feb 2015 03:25 minor feature: The --ideslave command line option has been replaced with a --ide-mode command line option with the same semantics.
0.9.1629 Nov 2014 19:05 minor feature: A new tactic sourceLocation that fills the current hole with the current source code span, if this information is available. If not, it raises an error.
ManageYou can also help out here by:
← Update project
or flagging this entry for moderator attention.