git.iko.soy/Idris-dev
on master help sign in
Rename to --optimise-nat-like-types.
11b4fb1Matus Tejiscak
CHANGELOG.md+6
compare with master
unifiedsplit
@@ -10,6 +10,12 @@
10 interfaces (i.e. types for names declared `export` and definitions of names
10 interfaces (i.e. types for names declared `export` and definitions of names
11 declared `public export`) are unchanged.
11 declared `public export`) are unchanged.
12
12
13+## Miscellaneous updates
14++ Compiler flag `--optimise-nat-like-types` enables compilation
15+ of `Nat`-like type families to big integers. A type family
16+ is `Nat`-like if, after erasure, it has two constructors,
17+ one nullary, the other one with exactly one recursive field.
18+
13# New in 1.3.1
19# New in 1.3.1
14
20
15## Tool updates
21## Tool updates
src/Idris/CmdOptions.hs+10−4
@@ -209,10 +209,16 @@ parseFlags = many $
209 <|> flag' (AddOpt PETransform) (long "partial-eval")
209 <|> flag' (AddOpt PETransform) (long "partial-eval")
210 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")
210 <|> flag' (RemoveOpt PETransform) (long "no-partial-eval" <> help "Switch off partial evaluation, mainly for debugging purposes")
211
211
212− <|> flag' (AddOpt GeneralisedNatHack) (long "opt-nat-likes"
212+ <|> flag' (AddOpt GeneralisedNatHack) (
213+ long "optimise-nat-like-types"
214+ <> long "optimize-nat-like-types"
213− <> help "Enable compilation of Nat-like types to bigints")
215+ <> help "Enable compilation of Nat-like types to bigints"
216+ )
214− <|> flag' (RemoveOpt GeneralisedNatHack) (long "no-opt-nat-likes"
217+ <|> flag' (RemoveOpt GeneralisedNatHack) (
218+ long "no-optimise-nat-like-types"
219+ <> long "no-optimize-nat-like-types"
215− <> help "Disable compilation of Nat-like types to bigints")
220+ <> help "Disable compilation of Nat-like types to bigints"
221+ )
216
222
217 <|> OptLevel <$> option auto (short 'O' <> long "level")
223 <|> OptLevel <$> option auto (short 'O' <> long "level")
218
224