<div dir="ltr"><div>Dear list,</div><div>I try to define a zip-with function without pattern matching through universal constructor eliminator for Lists.</div><div><br></div><div><div><font face="monospace, monospace">

<span style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">id</span> : {a : _} → {A : Set a} → A → A</font></div><div><font face="monospace, monospace">

<span style="color:rgb(34,34,34);font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">id</span> x = x</font></div></div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">data List {a} (A : Set a) : Set a where</font></div><div><font face="monospace, monospace"> nil : List A</font></div><div><font face="monospace, monospace"> cons : A → List A → List A</font></div><div><font face="monospace, monospace"><br></font></div><div><div><font face="monospace, monospace">fold : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → List A → (A → List A → ((B → C) → B → C) → (B → C) → B → C) → (B → C) → B → C</font></div><div><font face="monospace, monospace">fold nil _ fs s = fs s</font></div><div><font face="monospace, monospace">fold (cons x xs) f = f x xs (fold xs f)</font></div></div><div><font face="monospace, monospace"><br></font></div><div><font face="monospace, monospace">zip-with : {a b c : _} → {A : Set a} → {B : Set b} → {C : Set c} → (A → B → C) → List A → List B → List C</font></div></div><div><div><font face="monospace, monospace">zip-with f x y = fold x (λ ξ ξs _ _ _ → fold y (λ η ηs _ _ _ → cons (f ξ η) (zip-with f ξs ηs)) id nil) id nil</font></div></div><div><br></div><div>

<span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">But it fails termination checking.</span><br></div><div><span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><br></span></div><div><span style="text-align:start;text-indent:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline"><div><font face="monospace, monospace">Termination checking failed for the following functions:</font></div><div><font face="monospace, monospace">  zip-with</font></div><div><font face="monospace, monospace">Problematic calls:</font></div><div><font face="monospace, monospace">  zip-with f ξs ηs</font></div><div><br></div><div>I would not want to suppress <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">termination checking at all with {-# TERMINATING #-}.</span></div><div>What can I do here? Maybe it makes sense somehow to improve <span style="color:rgb(34,34,34);font-family:arial,sans-serif;font-size:small;font-style:normal;font-variant-ligatures:normal;font-variant-caps:normal;font-weight:400;letter-spacing:normal;text-align:start;text-indent:0px;text-transform:none;white-space:normal;word-spacing:0px;background-color:rgb(255,255,255);text-decoration-style:initial;text-decoration-color:initial;float:none;display:inline">termination checker for so obvious cases?</span></div></span></div></div>