/usr/share/doc/libghc-cryptol-doc/html/Cryptol-Symbolic-Prims.html is in libghc-cryptol-doc 2.2.6-1build1.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 | <!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>Cryptol.Symbolic.Prims</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_Cryptol-Symbolic-Prims.html");};
//]]>
</script></head><body><div id="package-header"><ul class="links" id="page-menu"><li><a href="src/Cryptol-Symbolic-Prims.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">cryptol-2.2.6: Cryptol: The Language of Cryptography</p></div><div id="content"><div id="module-header"><table class="info"><tr><th>Copyright</th><td>(c) 2013-2015 Galois, Inc.</td></tr><tr><th>License</th><td>BSD3</td></tr><tr><th>Maintainer</th><td>cryptol@galois.com</td></tr><tr><th>Stability</th><td>provisional</td></tr><tr><th>Portability</th><td>portable</td></tr><tr><th>Safe Haskell</th><td>None</td></tr><tr><th>Language</th><td>Haskell98</td></tr></table><p class="caption">Cryptol.Symbolic.Prims</p></div><div id="description"><p class="caption">Description</p><div class="doc empty"> </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"><a href="#v:traverseSnd">traverseSnd</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Functor.html#t:Functor">Functor</a> f => (a -> f b) -> (t, a) -> f (t, b)</li><li class="src short"><a href="#v:evalECon">evalECon</a> :: <a href="Cryptol-Prims-Syntax.html#t:ECon">ECon</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:selectV">selectV</a> :: (<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a>) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:replicateV">replicateV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:nth">nth</a> :: a -> [a] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> a</li><li class="src short"><a href="#v:nthV">nthV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:mapV">mapV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Bool.html#t:Bool">Bool</a> -> (<a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a>) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:catV">catV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:dropV">dropV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:takeV">takeV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:ecDemoteV">ecDemoteV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><span class="keyword">data</span> <a href="#t:TypeVal">TypeVal</a><ul class="subs"><li>= <a href="#v:TVBit">TVBit</a></li><li>| <a href="#v:TVSeq">TVSeq</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></li><li>| <a href="#v:TVStream">TVStream</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></li><li>| <a href="#v:TVTuple">TVTuple</a> [<a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a>]</li><li>| <a href="#v:TVRecord">TVRecord</a> [(<a href="Cryptol-Parser-AST.html#t:Name">Name</a>, <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a>)]</li><li>| <a href="#v:TVFun">TVFun</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></li></ul></li><li class="src short"><a href="#v:toTypeVal">toTypeVal</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Binary">Binary</a> = <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><span class="keyword">type</span> <a href="#t:Unary">Unary</a> = <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:arithBinary">arithBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:arithUnary">arithUnary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Unary">Unary</a></li><li class="src short"><a href="#v:sExp">sExp</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a></li><li class="src short"><a href="#v:sLg2">sLg2</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a></li><li class="src short"><a href="#v:cmpValue">cmpValue</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> a -> a) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> a -> a) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> a -> a</li><li class="src short"><a href="#v:cmpEq">cmpEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpNotEq">cmpNotEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpLt">cmpLt</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpGt">cmpGt</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpLtEq">cmpLtEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpGtEq">cmpGtEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:cmpBinary">cmpBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:errorV">errorV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:zeroV">zeroV</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:joinV">joinV</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:ecSplitV">ecSplitV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:infChunksOf">infChunksOf</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> [a] -> [[a]]</li><li class="src short"><a href="#v:finChunksOf">finChunksOf</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> [a] -> [[a]]</li><li class="src short"><a href="#v:logicBinary">logicBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a></li><li class="src short"><a href="#v:logicUnary">logicUnary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Unary">Unary</a></li><li class="src short"><a href="#v:fromThenV">fromThenV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:fromToV">fromToV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:fromThenToV">fromThenToV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></li><li class="src short"><a href="#v:addPoly">addPoly</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>]</li><li class="src short"><a href="#v:ites">ites</a> :: <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>]</li><li class="src short"><a href="#v:degree">degree</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a></li><li class="src short"><a href="#v:mdp">mdp</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> ([<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>], [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>])</li><li class="src short"><a href="#v:idx">idx</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a></li><li class="src short"><a href="#v:divx">divx</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> ([<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>], [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>])</li></ul></div><div id="interface"><h1>Documentation</h1><div class="top"><p class="src"><a name="v:traverseSnd" class="def">traverseSnd</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Functor.html#t:Functor">Functor</a> f => (a -> f b) -> (t, a) -> f (t, b) <a href="src/Cryptol-Symbolic-Prims.html#traverseSnd" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:evalECon" class="def">evalECon</a> :: <a href="Cryptol-Prims-Syntax.html#t:ECon">ECon</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#evalECon" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:selectV" class="def">selectV</a> :: (<a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a>) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#selectV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:replicateV" class="def">replicateV</a> <a href="src/Cryptol-Symbolic-Prims.html#replicateV" class="link">Source</a></p><div class="subs arguments"><p class="caption">Arguments</p><table><tr><td class="src">:: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a></td><td class="doc"><p>number of elements</p></td></tr><tr><td class="src">-> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a></td><td class="doc"><p>type of element</p></td></tr><tr><td class="src">-> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></td><td class="doc"><p>element</p></td></tr><tr><td class="src">-> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:nth" class="def">nth</a> :: a -> [a] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> a <a href="src/Cryptol-Symbolic-Prims.html#nth" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:nthV" class="def">nthV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#nthV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mapV" class="def">mapV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Bool.html#t:Bool">Bool</a> -> (<a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a>) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#mapV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:catV" class="def">catV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#catV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:dropV" class="def">dropV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#dropV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:takeV" class="def">takeV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#takeV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:ecDemoteV" class="def">ecDemoteV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#ecDemoteV" class="link">Source</a></p><div class="doc"><p>Make a numeric constant.
{ val, bits } (fin val, fin bits, bits >= width val) => [bits]</p></div></div><div class="top"><p class="src"><span class="keyword">data</span> <a name="t:TypeVal" class="def">TypeVal</a> <a href="src/Cryptol-Symbolic-Prims.html#TypeVal" class="link">Source</a></p><div class="doc"><p>An easy-to-use alternative representation for type <code><a href="Cryptol-Eval-Value.html#t:TValue">TValue</a></code>.</p></div><div class="subs constructors"><p class="caption">Constructors</p><table><tr><td class="src"><a name="v:TVBit" class="def">TVBit</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TVSeq" class="def">TVSeq</a> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TVStream" class="def">TVStream</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TVTuple" class="def">TVTuple</a> [<a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a>]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TVRecord" class="def">TVRecord</a> [(<a href="Cryptol-Parser-AST.html#t:Name">Name</a>, <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a>)]</td><td class="doc empty"> </td></tr><tr><td class="src"><a name="v:TVFun" class="def">TVFun</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a></td><td class="doc empty"> </td></tr></table></div></div><div class="top"><p class="src"><a name="v:toTypeVal" class="def">toTypeVal</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Prims.html#t:TypeVal">TypeVal</a> <a href="src/Cryptol-Symbolic-Prims.html#toTypeVal" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Binary" class="def">Binary</a> = <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#Binary" class="link">Source</a></p></div><div class="top"><p class="src"><span class="keyword">type</span> <a name="t:Unary" class="def">Unary</a> = <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#Unary" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:arithBinary" class="def">arithBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a> <a href="src/Cryptol-Symbolic-Prims.html#arithBinary" class="link">Source</a></p><div class="doc"><p>Models functions of type `{a} (Arith a) => a -> a -> a`</p></div></div><div class="top"><p class="src"><a name="v:arithUnary" class="def">arithUnary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Unary">Unary</a> <a href="src/Cryptol-Symbolic-Prims.html#arithUnary" class="link">Source</a></p><div class="doc"><p>Models functions of type `{a} (Arith a) => a -> a`</p></div></div><div class="top"><p class="src"><a name="v:sExp" class="def">sExp</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> <a href="src/Cryptol-Symbolic-Prims.html#sExp" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:sLg2" class="def">sLg2</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> <a href="src/Cryptol-Symbolic-Prims.html#sLg2" class="link">Source</a></p><div class="doc"><p>Ceiling (log_2 x)</p></div></div><div class="top"><p class="src"><a name="v:cmpValue" class="def">cmpValue</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> a -> a) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> a -> a) -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> a -> a <a href="src/Cryptol-Symbolic-Prims.html#cmpValue" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpEq" class="def">cmpEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpEq" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpNotEq" class="def">cmpNotEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpNotEq" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpLt" class="def">cmpLt</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpLt" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpGt" class="def">cmpGt</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpGt" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpLtEq" class="def">cmpLtEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpLtEq" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpGtEq" class="def">cmpGtEq</a> :: <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpGtEq" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:cmpBinary" class="def">cmpBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a> <a href="src/Cryptol-Symbolic-Prims.html#cmpBinary" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:errorV" class="def">errorV</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-String.html#t:String">String</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#errorV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:zeroV" class="def">zeroV</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#zeroV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:joinV" class="def">joinV</a> :: <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Eval-Value.html#t:TValue">TValue</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> -> <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#joinV" class="link">Source</a></p><div class="doc"><p>Join a sequence of sequences into a single sequence.</p></div></div><div class="top"><p class="src"><a name="v:ecSplitV" class="def">ecSplitV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#ecSplitV" class="link">Source</a></p><div class="doc"><p>Split implementation.</p></div></div><div class="top"><p class="src"><a name="v:infChunksOf" class="def">infChunksOf</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> [a] -> [[a]] <a href="src/Cryptol-Symbolic-Prims.html#infChunksOf" class="link">Source</a></p><div class="doc"><p>Split into infinitely many chunks</p></div></div><div class="top"><p class="src"><a name="v:finChunksOf" class="def">finChunksOf</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Prelude.html#t:Integer">Integer</a> -> [a] -> [[a]] <a href="src/Cryptol-Symbolic-Prims.html#finChunksOf" class="link">Source</a></p><div class="doc"><p>Split into finitely many chunks</p></div></div><div class="top"><p class="src"><a name="v:logicBinary" class="def">logicBinary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Binary">Binary</a> <a href="src/Cryptol-Symbolic-Prims.html#logicBinary" class="link">Source</a></p><div class="doc"><p>Merge two values given a binop. This is used for and, or and xor.</p></div></div><div class="top"><p class="src"><a name="v:logicUnary" class="def">logicUnary</a> :: (<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>) -> (<a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a> -> <a href="Cryptol-Symbolic-Value.html#t:SWord">SWord</a>) -> <a href="Cryptol-Symbolic-Prims.html#t:Unary">Unary</a> <a href="src/Cryptol-Symbolic-Prims.html#logicUnary" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromThenV" class="def">fromThenV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#fromThenV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromToV" class="def">fromToV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#fromToV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:fromThenToV" class="def">fromThenToV</a> :: <a href="Cryptol-Symbolic-Value.html#t:Value">Value</a> <a href="src/Cryptol-Symbolic-Prims.html#fromThenToV" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:addPoly" class="def">addPoly</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] <a href="src/Cryptol-Symbolic-Prims.html#addPoly" class="link">Source</a></p><div class="doc"><p>Add two polynomials</p></div></div><div class="top"><p class="src"><a name="v:ites" class="def">ites</a> :: <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] <a href="src/Cryptol-Symbolic-Prims.html#ites" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:degree" class="def">degree</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> <a href="src/Cryptol-Symbolic-Prims.html#degree" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:mdp" class="def">mdp</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> ([<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>], [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>]) <a href="src/Cryptol-Symbolic-Prims.html#mdp" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:idx" class="def">idx</a> :: [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> <a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a> <a href="src/Cryptol-Symbolic-Prims.html#idx" class="link">Source</a></p></div><div class="top"><p class="src"><a name="v:divx" class="def">divx</a> :: <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> <a href="file:///usr/share/doc/ghc-doc/html/libraries/base-4.8.2.0/Data-Int.html#t:Int">Int</a> -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>] -> ([<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>], [<a href="Cryptol-Symbolic-Value.html#t:SBool">SBool</a>]) <a href="src/Cryptol-Symbolic-Prims.html#divx" 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.16.1</p></div></body></html>
|