title: Is the evaluation strategy of Agda specified anywhere?
body: <p>Given that all Agda programs terminate, the evaluation strategy doesn't matter for denotational semantics but it does matter for performance (in case you ever run your Agda programs).</p>
  
  <p>So, what evaluation strategy does Agda use? Does using codata (♯, ♭) instead of data change evaluation strategy? Is there a way to force call-by-need aka lazy evaluation?</p>