There are three functions marked as non-terminating:
in Pi+/Coxeter/NonParametrized/Diamond.agda: diamond and diamond-full
in Pi+/Coxeter/NonParametrized/LehmerReduction.agda : Listℕ-to-LehmerProper
All three of them are of similar nature, and they terminate based on the same reason. Namely, when they are called with an argument l1 : Listℕ, they are calling themselves recursively on l2, which has the property that l1 ≅* l2. Relation ≅* has the property that, if l1 ≅* l2, then l2 is lexicographically smaller than l1.
Thus, we need to:
[ ] define the lexicographical order on lists
[ ] construct some mechanism which will be able to call the functions above using this order
Hopefully, this can be done in a generic way, to not bother with the details of the functions above (they are quite messy and I can modify them to fit in the generic interface myself).
There are three functions marked as non-terminating:
Pi+/Coxeter/NonParametrized/Diamond.agda:diamondanddiamond-fullPi+/Coxeter/NonParametrized/LehmerReduction.agda:Listℕ-to-LehmerProperAll three of them are of similar nature, and they terminate based on the same reason. Namely, when they are called with an argument
l1 : Listℕ, they are calling themselves recursively onl2, which has the property thatl1 ≅* l2. Relation≅*has the property that, ifl1 ≅* l2, thenl2is lexicographically smaller thanl1.Thus, we need to:
Hopefully, this can be done in a generic way, to not bother with the details of the functions above (they are quite messy and I can modify them to fit in the generic interface myself).