Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Document the classes that inhabit the various overloading classes. #1521

Merged
merged 2 commits into from
May 24, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
149 changes: 149 additions & 0 deletions docs/RefMan/OverloadedOperations.rst
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,28 @@ Equality
(===) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)
(!==) : {a, b} (Eq b) => (a -> b) -> (a -> b) -> (a -> Bit)


.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``fin n``, ``Eq a``
* - ``(a,b)``
- ``Eq a``, ``Eq b``



Comparisons
-----------

Expand All @@ -27,6 +49,27 @@ Comparisons
abs : {a} (Cmp a, Ring a) => a -> a


.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``fin n``, ``Cmp a``
* - ``(a,b)``
- ``Cmp a``, ``Cmp b``





Signed Comparisons
------------------

Expand All @@ -38,6 +81,17 @@ Signed Comparisons
(<=$) : {a} (SignedCmp a) => a -> a -> Bit
(>=$) : {a} (SignedCmp a) => a -> a -> Bit

.. list-table:: Instances

* - Type
- Condition
* - ``[n] Bit``
- ``fin n``, ``n >= 1``
* - ``[n] a``
- ``fin n``, ``SignedCmp a``, ``a /= Bit``
* - ``(a,b)``
- ``SignedCmp a``, ``SignedCmp b``


Zero
----
Expand All @@ -47,6 +101,27 @@ Zero
Zero
zero : {a} (Zero a) => a

.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] a``
- ``Zero a``
* - ``a -> b``
- ``Zero b``
* - ``(a,b)``
- ``Zero a``, ``Zero b``

Logical Operations
------------------

Expand All @@ -58,6 +133,21 @@ Logical Operations
(^) : {a} (Logic a) => a -> a -> a
complement : {a} (Logic a) => a -> a

.. list-table:: Instances

* - Type
- Condition
* - ``Bit``
-
* - ``[n] a``
- ``Logic a``
* - ``a -> b``
- ``Logic b``
* - ``(a,b)``
- ``Logic a``, ``Logic b``



Basic Arithmetic
----------------

Expand All @@ -71,6 +161,29 @@ Basic Arithmetic
negate : {a} (Ring a) => a -> a
(^^) : {a, e} (Ring a, Integral e) => a -> e -> a

.. list-table:: Instances

* - Type
- Condition
* - ``Integer``
-
* - ``Rational``
-
* - ``Z n``
- ``fin n``, ``n >= 1``
* - ``Float e p``
- ``ValidFloat e p``
* - ``[n] Bit``
- ``fin n``
* - ``[n] a``
- ``Ring a``, ``a /= Bit``
* - ``a -> b``
- ``Ring b``
* - ``(a,b)``
- ``Ring a``, ``Ring b``



Integral Operations
-------------------

Expand All @@ -84,6 +197,18 @@ Integral Operations
infFrom : {a} (Integral a) => a -> [inf]a
infFromThen : {a} (Integral a) => a -> a -> [inf]a

.. list-table:: Instances

* - Type
- Condition
* - ``Integer``
-
* - ``[n] Bit``
- ``fin n``





Division
--------
Expand All @@ -94,6 +219,20 @@ Division
recip : {a} (Field a) => a -> a
(/.) : {a} (Field a) => a -> a -> a


.. list-table:: Instances

* - Type
- Condition
* - ``Rational``
-
* - ``Z n``
- ``prime n``
* - ``Float e p``
- ``ValidFloat e p``



Rounding
--------

Expand All @@ -105,3 +244,13 @@ Rounding
trunc : {a} (Round a) => a -> Integer
roundAway : {a} (Round a) => a -> Integer
roundToEven : {a} (Round a) => a -> Integer


.. list-table:: Instances

* - Type
- Condition
* - ``Float e p``
- ``ValidFloat e p``


Binary file modified docs/RefMan/_build/doctrees/BasicSyntax.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/BasicTypes.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/Expressions.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/FFI.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/Modules.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/OverloadedOperations.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/RefMan.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/TypeDeclarations.doctree
Binary file not shown.
Binary file modified docs/RefMan/_build/doctrees/environment.pickle
Binary file not shown.
2 changes: 1 addition & 1 deletion docs/RefMan/_build/html/.buildinfo
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# Sphinx build info version 1
# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
config: 69485412ee215e2257ea16f8a42506fe
config: 49d6d89345e8bba027ef627e0adeb689
tags: 645f666f9bcd5a90fca523b33c5a78b7
Loading