<p>I finally found an answer <a href="https://docs.idris-lang.org/en/latest/reference/syntax-guide.html#totality" rel="nofollow noreferrer">here</a>.</p>
<p>@MaxNew was right; it's just a part of totality.  A function definition is not covering if there is a possible input which has not been handled in the pattern matching.</p>

CC BY-SA 4.0
2022-06-10T09:08:35.330Z
2022-06-10T09:08:35.330Z
MCLooyverse
<p>In <a href="https://github.com/idris-lang/Idris2" rel="nofollow noreferrer">Idris2</a>, I will sometimes get an error telling me that a function &quot;is not covering&quot;, which is apparently distinct from it not being total (and I do understand what a total function is).  I have not been able to find a reference to a &quot;covering function&quot; anywhere on Wikipedia, Wolfram, or any Stack Exchanges (except <a href="https://stackoverflow.com/questions/72114989/how-can-i-convince-idris-that-my-function-is-covering">here</a>).  When I <em>do</em> find references to it (in some Idris question), it is not explained what it actually means -- apparently everyone there just knows.</p>
<p>What I <em>do</em> find is something called a &quot;covering <strong>space</strong>&quot;, which is related to a &quot;covering map&quot;, but apparently a covering map is always continuous, so that can't be what Idris is talking about, since no function from ℕ to anything (for example) can be continuous.</p>

CC BY-SA 4.0
2022-06-07T16:30:33.913Z
Based on that other answer, it just means that a definition by cases doesn't cover all possible cases.
Max New
CC BY-SA 4.0
2022-06-07T23:25:48.060Z
@MaxNew That's what it looks like, but I don't know why it wouldn't just be called partial/non-total if that's what it's talking about.
MCLooyverse
CC BY-SA 4.0
2022-06-09T13:27:10.470Z
There are other reasons a function might be partial (such as if its definition uses a partial function). This is more informative, it tells you there is something specifically wrong with your patterns.
Max New
CC BY-SA 4.0
2022-06-09T21:49:33.440Z
@MaxNew Ah!  That makes sense!
MCLooyverse
<functional-programming><function><definitions>
What is a "Covering Function"?
MCLooyverse
# What is a "Covering Function"?

(Asked by: username_0 on 2022-06-07)

In [Idris2](https://github.com/idris-lang/Idris2), I will sometimes get an error telling me that a function "is not covering", which is apparently distinct from it not being total (and I do understand what a total function is). I have not been able to find a reference to a "covering function" anywhere on Wikipedia, Wolfram, or any Stack Exchanges (except [here](https://stackoverflow.com/questions/72114989/how-can-i-convince-idris-that-my-function-is-covering)). When I *do* find references to it (in some Idris question), it is not explained what it actually means -- apparently everyone there just knows.

What I *do* find is something called a "covering **space**", which is related to a "covering map", but apparently a covering map is always continuous, so that can't be what Idris is talking about, since no function from ℕ to anything (for example) can be continuous.

**Tags:** functional-programming, function, definitions
> **Comments:**
> **username_1**: Based on that other answer, it just means that a definition by cases doesn't cover all possible cases.  
> **username_0**: @MaxNew That's what it looks like, but I don't know why it wouldn't just be called partial/non-total if that's what it's talking about.  
> **username_1**: There are other reasons a function might be partial (such as if its definition uses a partial function). This is more informative, it tells you there is something specifically wrong with your patterns.  
> **username_0**: @MaxNew Ah!  That makes sense!  

---

## 1 answers

### Answer by username_0 on 2022-06-10. Score: 1 | Accepted answer

I finally found an answer [here](https://docs.idris-lang.org/en/latest/reference/syntax-guide.html#totality).

@MaxNew was right; it's just a part of totality. A function definition is not covering if there is a possible input which has not been handled in the pattern matching.


---

