A definition without a clause for each pattern may not terminate with a higher inductive type. Consider the join list defined as an inductive type with four equality constructors:
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
data JList (A : Set) : Set where
[] : JList A
[_] : A → JList A
_⧺_ : (xs ys : JList A) → JList A
⧺-unit-l : (ys : JList A) → [] ⧺ ys ≡ ys
⧺-unit-r : (xs : JList A) → xs ⧺ [] ≡ xs
⧺-assoc : (xs ys zs : JList A) → (xs ⧺ ys) ⧺ zs ≡ xs ⧺ (ys ⧺ zs)
trunc : isSet (JList A)
Then, type-checking the following definition (for concatenation) does not terminate.
_++_ : {A : Set} (xs ys : JList A) → JList A
[] ++ ys = {!!}
xs ++ [] = {!!}
xs ++ ys = {!!}
However, after removing ⧺-unit-l and ⧺-unit-r, the function _++_ can be type-checked again. Listing all possible cases also works.
Tested with Agda 2.7.01, 2.8 (the latest commit on master) on macOS 15.0.1.
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4