I've heard the phrase used in relation to comparing proof assistants, but I don't understand what it means.
For example, for introducing an instance of coinductive types, Agda uses destructors and Idris uses constructors...and having used Idris I was thinking that Agda's approach was non-canonical in that the terms can't be broken down into constructors nor do they always progress to whnf. But I have been told this is not correct. So what is a non-canonical term?
To give an example (following ice1000's post):
Yes (to ice1000), this is the question. And here's an example in Idris:
data CoNat: Type where Zero : CoNat Succ : Inf CoNat -> CoNat
With corresponding code in Agda:
record ℕ∞ : Set where coinductive field prd∞ : Maybe ℕ∞
But Agda has elements that don't appear in the Idris version
record ℕ∞ : Set where coinductive field prd∞ : Maybe ℕ∞ +∞ : ℕ∞ → ℕ∞ → ℕ∞ prd∞ (m +∞ n) with prd∞ m ... | nothing = prd∞ n ... | just m' = just (m' +∞ n) ∞ : ℕ∞ prd∞ ∞ = just ∞ noncanonical? : ℕ∞ noncanonical? = ∞ +∞ ∞
So I was thinking that such elements must be non-canonical as they are not present in the Idris version!! If they are not non-canonical because they are defined in terms of the 'destructors' then what would be an example of a non-canonical instance???