> Multiplicity 0 removes the value from the runtime avoiding allocations and gar...

		dwohnitmok on Jan 25, 2022 \| parent \| context \| favorite \| on: Idris 2: Quantitative Type Theory in Practice > Multiplicity 0 removes the value from the runtime avoiding allocations and garbage collection. Does this apply even for compile-time evaluation? I'm not sure of the specifics of how Idris does compile-time evaluation vs runtime evaluation.