mirror of
https://github.com/idris-lang/Idris2.git
synced 2025-01-07 08:18:12 +03:00
ab2012a7dc
No idea what happened there. Maybe a minor change in the input? Anyway, this updates it as it should be.
42 lines
1.4 KiB
Plaintext
42 lines
1.4 KiB
Plaintext
1/1: Building NatOpts (NatOpts.idr)
|
|
Main> Main.doPlus ==> [{arg:0}, {arg:1}];
|
|
Compile time tree: [0] (Prelude.Types.plus {arg:0}[0] {arg:1}[1])
|
|
Run time tree: Error: ""
|
|
RigW
|
|
Erasable args: []
|
|
Detaggable arg types: []
|
|
Specialise args: []
|
|
Inferrable args: []
|
|
Compiled: [{arg:0}, {arg:1}]: (+Integer [!{arg:0}, !{arg:1}])
|
|
Refers to: [Prelude.Types.plus]
|
|
Refers to (runtime): []
|
|
Flags: [covering]
|
|
Size change: Prelude.Types.plus: [Just (0, Same), Just (1, Same)]
|
|
Main> Main.doMinus ==> [{arg:0}, {arg:1}];
|
|
Compile time tree: [0] (Prelude.Types.minus {arg:0}[0] {arg:1}[1])
|
|
Run time tree: Error: ""
|
|
RigW
|
|
Erasable args: []
|
|
Detaggable arg types: []
|
|
Specialise args: []
|
|
Inferrable args: []
|
|
Compiled: [{arg:0}, {arg:1}]: (Prelude.Types.prim__integerToNat [(-Integer [!{arg:0}, !{arg:1}])])
|
|
Refers to: [Prelude.Types.minus]
|
|
Refers to (runtime): [Prelude.Types.prim__integerToNat]
|
|
Flags: [covering]
|
|
Size change: Prelude.Types.minus: [Just (0, Same), Just (1, Same)]
|
|
Main> Main.doMult ==> [{arg:0}, {arg:1}];
|
|
Compile time tree: [0] (Prelude.Types.mult {arg:0}[0] {arg:1}[1])
|
|
Run time tree: Error: ""
|
|
RigW
|
|
Erasable args: []
|
|
Detaggable arg types: []
|
|
Specialise args: []
|
|
Inferrable args: []
|
|
Compiled: [{arg:0}, {arg:1}]: (*Integer [!{arg:0}, !{arg:1}])
|
|
Refers to: [Prelude.Types.mult]
|
|
Refers to (runtime): []
|
|
Flags: [covering]
|
|
Size change: Prelude.Types.mult: [Just (0, Same), Just (1, Same)]
|
|
Main> Bye for now!
|