Modulo function for Natural numbers?

Hello all,

I was wondering if anyone has been able to write a modulo function for Natural numbers in Dhall? It’s not entirely clear to me whether this is actually possible without recursion. I’ve read the section of the docs on translating recursive code to dhall but found it was stretching my rather limited math talent.

Should anyone need this in the future, I’ve written a modulo function by riding off the back of the recursive List type:

let Prelude =

let modulo =
    λ(a : Natural) ->
    λ(n : Natural) ->
        let flattened = Prelude.List.generate a Natural (λ(_ : Natural) -> n)
        let ff =
            λ(_ : Natural) →
            λ(acc : Natural) →
            if Prelude.Natural.lessThan acc n
                then acc
                else Natural/subtract n acc
        in List/fold

I imagine this is not exactly the most optimal implementation but it works for my purposes for the time being.

Some more code:

Division with remainder, integer binary logarithm, integer square root, integer power, greatest common divisor