<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd"><html xmlns="http://www.w3.org/1999/xhtml"><head><meta http-equiv="Content-Type" content="text/html; charset=UTF-8" /><title>Agda.TypeChecking.Free</title><link href="ocean.css" rel="stylesheet" type="text/css" title="Ocean" /><script src="haddock-util.js" type="text/javascript"></script><script type="text/javascript">//<![CDATA[
window.onload = function () {pageLoad();setSynopsis("mini_Agda-TypeChecking-Free.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Agda-TypeChecking-Free.html">Source</a></li><li><a href="index.html">Contents</a></li><li><a href="doc-index.html">Index</a></li></ul><p class="caption">Agda-2.3.2.1: A dependently typed functional programming language and proof assistant</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Safe Haskell</th><td>None</td></tr></table><p class="caption">Agda.TypeChecking.Free</p></div><div id="description"><p class="caption">Description</p><div class="doc"><p>Computing the free variables of a term.
</p></div></div><div id="synopsis"><p id="control.syn" class="caption expander" onclick="toggleSection('syn')">Synopsis</p><ul id="section.syn" class="hide" onclick="toggleSection('syn')"><li class="src short"><span class="keyword">data</span> <a href="#t:FreeVars">FreeVars</a> = <a href="#v:FV">FV</a> {<ul class="subs"><li><a href="#v:stronglyRigidVars">stronglyRigidVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li><a href="#v:weaklyRigidVars">weaklyRigidVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li><a href="#v:flexibleVars">flexibleVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li><a href="#v:irrelevantVars">irrelevantVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li><a href="#v:unusedVars">unusedVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li></ul>}</li><li class="src short"><span class="keyword">class</span> <a href="#t:Free">Free</a> a </li><li class="src short"><a href="#v:freeVars">freeVars</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => a -> <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a></li><li class="src short"><a href="#v:allVars">allVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li class="src short"><a href="#v:relevantVars">relevantVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li class="src short"><a href="#v:rigidVars">rigidVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></li><li class="src short"><a href="#v:freeIn">freeIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:isBinderUsed">isBinderUsed</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:freeInIgnoringSorts">freeInIgnoringSorts</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:freeInIgnoringSortAnn">freeInIgnoringSortAnn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:relevantIn">relevantIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><a href="#v:relevantInIgnoringSortAnn">relevantInIgnoringSortAnn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:Occurrence">Occurrence</a> <ul class="subs"><li>= <a href="#v:NoOccurrence">NoOccurrence</a> </li><li>| <a href="#v:Irrelevantly">Irrelevantly</a> </li><li>| <a href="#v:StronglyRigid">StronglyRigid</a> </li><li>| <a href="#v:WeaklyRigid">WeaklyRigid</a> </li><li>| <a href="#v:Flexible">Flexible</a> </li><li>| <a href="#v:Unused">Unused</a> </li></ul></li><li class="src short"><a href="#v:occurrence">occurrence</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-TypeChecking-Free.html#t:Occurrence">Occurrence</a></li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:FreeVars" class="def">FreeVars</a> <a href="src/Agda-TypeChecking-Free.html#FreeVars" class="link">Source</a></p><div class="doc"><p>The distinction between rigid and strongly rigid occurrences comes from:
Jason C. Reed, PhD thesis, 2009, page 96 (see also his LFMTP 2009 paper)
</p><p>The main idea is that x = t(x) is unsolvable if x occurs strongly rigidly
in t. It might have a solution if the occurrence is not strongly rigid, e.g.
</p><p>x = f -> suc (f (x ( y -> k))) has x = f -> suc (f (suc k))
</p><dl><dt>Jason C. Reed, PhD thesis, page 106</dt><dd>
</dd></dl><p>Free variables of a term, (disjointly) partitioned into strongly and
and weakly rigid variables, flexible variables and irrelevant variables.
</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:FV" class="def">FV</a></td><td class="doc empty"> </td></tr><tr><td colspan="2"><div class="subs fields"><p class="caption">Fields</p><dl><dt class="src"><a name="v:stronglyRigidVars" class="def">stronglyRigidVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></dt><dd class="doc"><p>variables at top and under constructors
</p></dd><dt class="src"><a name="v:weaklyRigidVars" class="def">weaklyRigidVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></dt><dd class="doc"><p>ord. rigid variables, e.g., in arguments of variables
</p></dd><dt class="src"><a name="v:flexibleVars" class="def">flexibleVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></dt><dd class="doc"><p>variables occuring in arguments of metas. These are potentially free, depending how the meta variable is instantiated.
</p></dd><dt class="src"><a name="v:irrelevantVars" class="def">irrelevantVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></dt><dd class="doc"><p>variables in irrelevant arguments and under a <code>DontCare</code>, i.e., in irrelevant positions
</p></dd><dt class="src"><a name="v:unusedVars" class="def">unusedVars</a> :: <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a></dt><dd class="doc"><p>variables in <code><a href="Agda-Syntax-Common.html#v:UnusedArg">UnusedArg</a></code>uments
</p></dd></dl><div class="clear"></div></div></td></tr></table></div></div><div class="top"><p class="src"><span class="keyword">class</span> <a name="t:Free" class="def">Free</a> a <a href="src/Agda-TypeChecking-Free.html#Free" class="link">Source</a></p><div class="subs instances"><p id="control.i:Free" class="caption collapser" onclick="toggleSection('i:Free')">Instances</p><div id="section.i:Free" class="show"><table><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:ClauseBody">ClauseBody</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:LevelAtom">LevelAtom</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:PlusLevel">PlusLevel</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:Level">Level</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:Sort">Sort</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:Type">Type</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> <a href="Agda-Syntax-Internal.html#t:Term">Term</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> [a]</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Maybe.html#t:Maybe">Maybe</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Common.html#t:Arg">Arg</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Common.html#t:Dom">Dom</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Internal.html#t:Tele">Tele</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src"><a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (<a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a)</td><td class="doc empty"> </td></tr><tr><td class="src">(<a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a, <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> b) => <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> (a, b)</td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:freeVars" class="def">freeVars</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => a -> <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a><a href="src/Agda-TypeChecking-Free.html#freeVars" class="link">Source</a></p><div class="doc"><p>Doesn't go inside solved metas, but collects the variables from a
metavariable application <code>X ts</code> as <code>flexibleVars</code>.
</p></div></div><div class="top"><p class="src"><a name="v:allVars" class="def">allVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a><a href="src/Agda-TypeChecking-Free.html#allVars" class="link">Source</a></p><div class="doc"><p><code>allVars fv</code> includes irrelevant variables.
</p></div></div><div class="top"><p class="src"><a name="v:relevantVars" class="def">relevantVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a><a href="src/Agda-TypeChecking-Free.html#relevantVars" class="link">Source</a></p><div class="doc"><p>All but the irrelevant variables.
</p></div></div><div class="top"><p class="src"><a name="v:rigidVars" class="def">rigidVars</a> :: <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-Utils-VarSet.html#t:VarSet">VarSet</a><a href="src/Agda-TypeChecking-Free.html#rigidVars" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freeIn" class="def">freeIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#freeIn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:isBinderUsed" class="def">isBinderUsed</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Internal.html#t:Abs">Abs</a> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#isBinderUsed" class="link">Source</a></p><div class="doc"><p>Is the variable bound by the abstraction actually used?
</p></div></div><div class="top"><p class="src"><a name="v:freeInIgnoringSorts" class="def">freeInIgnoringSorts</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#freeInIgnoringSorts" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:freeInIgnoringSortAnn" class="def">freeInIgnoringSortAnn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#freeInIgnoringSortAnn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:relevantIn" class="def">relevantIn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#relevantIn" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:relevantInIgnoringSortAnn" class="def">relevantInIgnoringSortAnn</a> :: <a href="Agda-TypeChecking-Free.html#t:Free">Free</a> a => <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> a -> <a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Bool.html#t:Bool">Bool</a><a href="src/Agda-TypeChecking-Free.html#relevantInIgnoringSortAnn" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:Occurrence" class="def">Occurrence</a> <a href="src/Agda-TypeChecking-Free.html#Occurrence" class="link">Source</a></p><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:NoOccurrence" class="def">NoOccurrence</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Irrelevantly" class="def">Irrelevantly</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:StronglyRigid" class="def">StronglyRigid</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:WeaklyRigid" class="def">WeaklyRigid</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Flexible" class="def">Flexible</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:Unused" class="def">Unused</a></td><td class="doc empty"> </td></tr></table></div><div class="subs instances"><p id="control.i:Occurrence" class="caption collapser" onclick="toggleSection('i:Occurrence')">Instances</p><div id="section.i:Occurrence" class="show"><table><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Data-Eq.html#t:Eq">Eq</a> <a href="Agda-TypeChecking-Free.html#t:Occurrence">Occurrence</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a href="/usr/share/doc/ghc/html/libraries/base-4.5.1.0/Text-Show.html#t:Show">Show</a> <a href="Agda-TypeChecking-Free.html#t:Occurrence">Occurrence</a></td><td class="doc empty"> </td></tr></table></div></div></div><div class="top"><p class="src"><a name="v:occurrence" class="def">occurrence</a> :: <a href="Agda-Syntax-Common.html#t:Nat">Nat</a> -> <a href="Agda-TypeChecking-Free.html#t:FreeVars">FreeVars</a> -> <a href="Agda-TypeChecking-Free.html#t:Occurrence">Occurrence</a><a href="src/Agda-TypeChecking-Free.html#occurrence" class="link">Source</a></p></div></div></div><div id="footer"><p>Produced by <a href="http://www.haskell.org/haddock/">Haddock</a> version 2.11.0</p></div></body></html>
