4 ms·

I've never been aware of whether Agda is CBN or CBV because it actually doesn't matter (!). In a pure, terminating language like Agda evaluation is "confluent"

by tel 12y ago

I've never been aware of whether Agda is CBN or CBV because it actually doesn't matter (!). In a pure, terminating language like Agda evaluation is "confluent" which means that CBV and CBN evaluations are identical.

Peaker 12y ago
Identical up to one algorithm taking a few seconds, and another taking as long as the universe has been alive :)
- tel 12y ago
  Who runs Agda code anyway? :)
eru 12y ago
Not only CBV and CBN, but also strict evaluation.