Stream: Beginner Questions

Topic: Making the fun package support recursion through datatypes

irvin (Jan 29 2026 at 10:56):

Is there a way to make it such that the function package generates provable termination conditions when the recursive function is passed through a datatype? e.g. a function like this

function test :: "nat ⇒ nat" where
"test n = (if n = 0 then 0 else
          hd (map (λf. f (n - 1)) [test]))"

Last updated: Feb 12 2026 at 20:37 UTC