<blockquote>
<p>Why does where appear in the middle of the lambda function definition?,</p>
</blockquote>
<p>Quoting <a href="https://agda.readthedocs.io/en/v2.6.1/language/lambda-abstraction.html" rel="nofollow noreferrer">the docs</a>:</p>
<blockquote>
<p>Anonymous pattern matching functions can be defined using one of the
two following syntaxes:</p>
<p><code>\ { p11 .. p1n -&gt; e1 ; … ; pm1 .. pmn -&gt; em }</code></p>
<p><code>\ where   p11 .. p1n -&gt; e1   …   pm1 .. pmn -&gt; em</code></p>
</blockquote>
<p>So <code>λ where</code> is an anonymous pattern matching function. <code>force</code> is the field of <a href="https://github.com/agda/agda-stdlib/blob/14577d5f187329c8eef5997b5bc2d30af1955aad/src/Codata/Thunk.agda#L17" rel="nofollow noreferrer"><code>Thunk</code></a> and <code>.force</code> is a <a href="https://agda.readthedocs.io/en/v2.6.1/language/copatterns.html" rel="nofollow noreferrer">copattern</a> in postfix notation (originally I said nonsense here, but thanks to @<strong>Cactus</strong> it's now fixed, see <a href="https://stackoverflow.com/a/63013330/3237465">his answer</a>).</p>
<blockquote>
<p>Also, is there a place where I can find documentation to use &quot;Codata&quot; and proofs with it? Thanks!</p>
</blockquote>
<p>Check out these papers</p>
<ol>
<li><a href="https://arxiv.org/pdf/1406.2059" rel="nofollow noreferrer">Normalization by Evaluation in the Delay Monad
A Case Study for Coinduction via Copatterns and Sized Types</a></li>
<li><a href="http://www.cse.chalmers.se/%7Eabela/jlamp17.pdf" rel="nofollow noreferrer">Equational Reasoning about Formal Languages in Coalgebraic Style</a></li>
<li><a href="https://cs.ru.nl/%7Enweide/AgdaSizedTypes.pdf" rel="nofollow noreferrer">Guarded Recursion in Agda via Sized Types</a></li>
</ol>
What is `where .force`?
<p>I've been playing around with the idea of writing programs that run on Streams and properties with them, but I feel that I am stuck even with the simplest of things. When I look at the definition of <code>repeat</code> in <code>Codata/Streams</code> in the standard library, I find a construction that I haven't seen anywhere in Agda: <code>λ where .force →</code>.</p>
<p>Here, an excerpt of a Stream defined with this weird feature:</p>
<pre><code>repeat : ∀ {i} → A → Stream A i
repeat a = a ∷ λ where .force → repeat a
</code></pre>
<p>Why does <code>where</code> appear in the middle of the lambda function definition?, and what is the purpose of <code>.force</code> if it is never used?</p>
<p>I might be asking something that is in the documentation, but I can't figure out how to search for it.</p>
<p>Also, is there a place where I can find documentation to use &quot;Codata&quot; and proofs with it? Thanks!</p>