Skip to main content

Browse the archive

https://github.com/coq-ext-lib/coq-ext-lib
05 April 2024, 22:27:30 UTC
Raw File
Tip revision: 4e16cb58bb743938ce27de4155ca97a43796db45 authored by Yishuai Li on 17 January 2024, 23:01:51 UTC
Update templates
Tip revision: 4e16cb5
ExtLib.Structures.Functor.html 
<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">

<head>
<meta http-equiv="Content-Type" content="text/html;charset=utf-8" />
<link href="resources/coqdoc.css" rel="stylesheet" type="text/css" />
<link href="resources/coqdocjs.css" rel="stylesheet" type="text/css"/>
<script type="text/javascript" src="resources/config.js"></script>
<script type="text/javascript" src="resources/coqdocjs.js"></script>
</head>

<body onload="document.getElementById('content').focus()">
  <div id="header">
    <span class="left">
      <span class="modulename"> <script> document.write(document.title) </script> </span>
    </span>

    <span class="button" id="toggle-proofs"></span>

    <span class="right">
      <a href="../">Project Page</a>
      <a href="./indexpage.html"> Index </a>
      <a href="./toc.html"> Table of Contents </a>
    </span>
</div>
    <div id="content" tabindex="-1" onblur="document.getElementById('content').focus()">
    <div id="main">
<h1 class="libtitle">ExtLib.Structures.Functor</h1>

<div class="code">
<span class="id" title="keyword">Require</span> <span class="id" title="keyword">Import</span> <a class="idref" href="ExtLib.Core.Any.html#"><span class="id" title="library">ExtLib.Core.Any</span></a>.<br/>

<br/>
<span class="id" title="keyword">Set Implicit Arguments</span>.<br/>
<span class="id" title="keyword">Set</span> <span class="id" title="keyword">Strict</span> <span class="id" title="keyword">Implicit</span>.<br/>

<br/>
<span class="id" title="var">Polymorphic</span> <span class="id" title="keyword">Class</span> <a name="Functor"><span class="id" title="record">Functor@</span></a>{<span class="id" title="var">d</span> <span class="id" title="var">c</span>} (<span class="id" title="var">F</span> : <span class="id" title="var">Type@</span>{<span class="id" title="var">d</span>} <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <span class="id" title="var">Type@</span>{<span class="id" title="var">c</span>}) : <span class="id" title="keyword">Type</span> :=<br/>
{ <a name="fmap"><span class="id" title="projection">fmap</span></a> : <span class="id" title="keyword">forall</span> {<span class="id" title="var">A</span> <span class="id" title="var">B</span> : <span class="id" title="var">Type@</span>{<span class="id" title="var">d</span>}}, <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">(</span></a><a class="idref" href="ExtLib.Structures.Functor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#B"><span class="id" title="variable">B</span></a><a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">)</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#A"><span class="id" title="variable">A</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#F"><span class="id" title="variable">F</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#B"><span class="id" title="variable">B</span></a> }.<br/>

<br/>
<span class="id" title="var">Polymorphic</span> <span class="id" title="keyword">Definition</span> <a name="ID"><span class="id" title="definition">ID@</span></a>{<span class="id" title="var">d</span>} {<span class="id" title="var">T</span> : <span class="id" title="var">Type@</span>{<span class="id" title="var">d</span>}} (<span class="id" title="var">f</span> : <a class="idref" href="ExtLib.Structures.Functor.html#T"><span class="id" title="variable">T</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#1c93e43e07fbeaeb6a625cb6614beb5d"><span class="id" title="notation">-&gt;</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#T"><span class="id" title="variable">T</span></a>) : <span class="id" title="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="id" title="keyword">forall</span> <span class="id" title="var">x</span> : <a class="idref" href="ExtLib.Structures.Functor.html#T"><span class="id" title="variable">T</span></a>, <a class="idref" href="ExtLib.Structures.Functor.html#f"><span class="id" title="variable">f</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#x"><span class="id" title="variable">x</span></a> <a class="idref" href="http://coq.inria.fr/distrib/V8.9.1/stdlib//Coq.Init.Logic.html#6cd0f7b28b6092304087c7049437bb1a"><span class="id" title="notation">=</span></a> <a class="idref" href="ExtLib.Structures.Functor.html#x"><span class="id" title="variable">x</span></a>.<br/>

<br/>
<span class="id" title="keyword">Module</span> <a name="FunctorNotation"><span class="id" title="module">FunctorNotation</span></a>.<br/>
&nbsp;&nbsp;<span class="id" title="keyword">Notation</span> <a name="c90c765f14411304537ea486ccacb191"><span class="id" title="notation">&quot;</span></a>f &lt;$&gt; x" := (@<a class="idref" href="ExtLib.Structures.Functor.html#fmap"><span class="id" title="method">fmap</span></a> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">_</span> <span class="id" title="var">f</span> <span class="id" title="var">x</span>) (<span class="id" title="tactic">at</span> <span class="id" title="keyword">level</span> 52, <span class="id" title="tactic">left</span> <span class="id" title="keyword">associativity</span>).<br/>
<span class="id" title="keyword">End</span> <a class="idref" href="ExtLib.Structures.Functor.html#FunctorNotation"><span class="id" title="module">FunctorNotation</span></a>.<br/>
</div>
</div>
<div id="footer">
  Generated by <a href="http://coq.inria.fr/">coqdoc</a> and improved with <a href="https://github.com/tebbi/coqdocjs">CoqdocJS</a>
</div>
</div>
</body>

</html>
back to top