Termination-checking substitution via (monadic) jo

Question

I'm using sized types, and have a substitution function for typed terms which termination-checks if I give a definition directly, but not if I factor it via (monadic) join and fmap.

{-# OPTIONS --sized-types #-}

module Subst where

   open import Size

To show the problem, it's enough to have unit and sums. I have data types of Trie and Term, and I use tries with a codomain of Term inside Term, as part of the elimination form for sums.

   data Type : Set where
                      

            

标签： monads substitution termination agda

举报

Answer 1

Give join the following type:

join : ∀ {ι A Γ τ} → Term (Term A) {ι} Γ τ → Term A Γ τ

(from gallais' comment above).