Commit Graph

11 Commits

Author SHA1 Message Date
Stiopa Koltsov
7264d40c56 Make isElem, DecEq public, not just export
... so they could be used in proof search.

Follow-up to #942
2021-01-18 10:37:57 +00:00
Denis Buzdalov
4364793484 Type definition from Decidable.Equality was moved to a separate module
This is done to make able for `Data.*` modules of datatypes declared in
prelude to import modules that have their own definitions of `DecEq`
inside them (i.e. modules of datatypes declared in the `base`).
2020-12-04 19:09:05 +00:00
G. Allais
5e799563fa
[ contrib ] adding Data.Container (#781) 2020-11-27 15:29:19 +00:00
G. Allais
d105dd11a7
[ breaking ] remove List1 related ambiguities (#690) 2020-09-22 15:07:40 +01:00
G. Allais
937aa8fc43
[ refactor ] introducing Namespace (#638)
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the underlying representation of
  namespaces rather than say what we mean (using `isSuffixOf` to mean
  `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report #616 (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementation when
  showing / pretty-printing namespaces

This PR introduces a `Namespace` newtype containing a list of strings.
Nested namespaces are still stored in reverse order but the exposed
interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-05 09:41:31 +01:00
Guillaume ALLAIS
529944267b Revert "[ refactor ] Introducing Namespace and ModuleIdent (#631)"
This reverts commit 481dc431e7.
2020-09-04 09:16:06 +01:00
G. Allais
481dc431e7
[ refactor ] Introducing Namespace and ModuleIdent (#631)
Until now namespaces were stored as (reversed) lists of strings.
It led to:

* confusing code where we work on the representation rather than say
  what we mean (e.g. using `isSuffixOf` to mean `isParentOf`)

* potentially introducing errors by not respecting the invariant cf.
  bug report #616 (but also name generation in the scheme backend
  although that did not lead to bugs as it was self-consistent AFAICT)

* ad-hoc code to circumvent overlapping interface implementations when
  showing / pretty-printing namespaces

This introduces a Namespace newtype containing non-empty lists of
strings. Nested namespaces are still stored in reverse order but the
exposed interface aims to support programming by saying what we mean
(`isParentOf`, `isApproximationOf`, `X <.> Y` computes to `X.Y`, etc.)
irrespective of the underlying representation.
2020-09-02 20:05:33 +01:00
Ohad Kammar
915b7bea38 Add various instances from stdlib interfaces (Eq, Ord, DecEq)
For Void and Either

This is because I ended up using them elsewhere, so why not include them in the stdlib.

Also expose left/rightInjective functions, as are used in the DecEq proofs.
2020-07-26 10:47:38 +01:00
Nick Drozd
7d1ee9dd08 Simplify Equality 2020-07-07 10:48:23 +01:00
Nick Drozd
7c923944ae Add %default total to a few modules 2020-07-07 10:48:23 +01:00
Edwin Brady
dec7dff622 Add libraries 2020-05-18 14:00:08 +01:00