~helmut/bidiragda.git
6 months agoGeneric.toList-fromList is Data.Vec.Properties.toList∘fromList master
Helmut Grohne [Sun, 31 Mar 2019 20:36:21 +0000 (22:36 +0200)]
Generic.toList-fromList is Data.Vec.Properties.toList∘fromList

6 months agoGeneric.just-injective is Data.Maybe.just-injective
Helmut Grohne [Sun, 31 Mar 2019 20:01:56 +0000 (22:01 +0200)]
Generic.just-injective is Data.Maybe.just-injective

6 months agoFinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookup∘update′
Helmut Grohne [Sun, 31 Mar 2019 19:56:30 +0000 (21:56 +0200)]
FinMap.lemma-lookupM-delete is another variant of Data.Vec.Properties.lookup∘update′

6 months agoFinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate
Helmut Grohne [Sun, 31 Mar 2019 19:47:21 +0000 (21:47 +0200)]
FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Properties.lookup∘tabulate

6 months agoFinMap.lemma-tabulate-∘ is also known as Data.Vec.Properties.tabulate-cong
Helmut Grohne [Sun, 31 Mar 2019 19:23:11 +0000 (21:23 +0200)]
FinMap.lemma-tabulate-∘ is also known as Data.Vec.Properties.tabulate-cong

6 months agoreplace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicate
Helmut Grohne [Sun, 31 Mar 2019 19:14:50 +0000 (21:14 +0200)]
replace FinMap.lemma-lookupM-empty with Data.Vec.Properties.lookup-replicate

10 months agoport to agda/2.5.4.1 and agda-stdlib/0.17
Helmut Grohne [Sun, 25 Nov 2018 10:29:53 +0000 (11:29 +0100)]
port to agda/2.5.4.1 and agda-stdlib/0.17

10 months agoremove unused imports
Helmut Grohne [Sun, 25 Nov 2018 10:27:39 +0000 (11:27 +0100)]
remove unused imports

These will happen to break with later agda-stdlib releases.

10 months agomake the setoid parameter to sequenceV-cong explicit
Helmut Grohne [Sun, 25 Nov 2018 09:59:34 +0000 (10:59 +0100)]
make the setoid parameter to sequenceV-cong explicit

Later versions of agda will be unable to infer it unambiguously.

10 months agoreorganize equality imports
Helmut Grohne [Sun, 25 Nov 2018 09:35:23 +0000 (10:35 +0100)]
reorganize equality imports

Since we are working with multiple setoids now, it makes more sense to
qualify their members. Follow the "as P" pattern from the standard
library. Also stop importing those symbols from Relation.Binary.Core as
later agda-stdlib versions will move them away. Rather than EqSetoid or
PropEq, use P.setoid consistently.

10 months agofix missing import of "length"
Helmut Grohne [Sun, 25 Nov 2018 07:54:51 +0000 (08:54 +0100)]
fix missing import of "length"

Broken in parent commit.

21 months agolength-replicate is now upstream as well
Helmut Grohne [Tue, 2 Jan 2018 04:33:53 +0000 (05:33 +0100)]
length-replicate is now upstream as well

21 months agoremove lemma-lookupM-insert-other in favour of lookup∘update′
Helmut Grohne [Tue, 2 Jan 2018 04:14:32 +0000 (05:14 +0100)]
remove lemma-lookupM-insert-other in favour of lookup∘update′

21 months agoremove lemma-lookupM-insert in favour of lookup∘update
Helmut Grohne [Tue, 2 Jan 2018 04:01:56 +0000 (05:01 +0100)]
remove lemma-lookupM-insert in favour of lookup∘update

21 months agofix compilation with agda 2.5.3, agda-stdlib 0.14
Helmut Grohne [Mon, 1 Jan 2018 18:51:00 +0000 (19:51 +0100)]
fix compilation with agda 2.5.3, agda-stdlib 0.14

3 years agofix compilation with agda 2.5.1, agda-stdlib 0.12
Helmut Grohne [Tue, 21 Jun 2016 15:50:07 +0000 (17:50 +0200)]
fix compilation with agda 2.5.1, agda-stdlib 0.12

4 years agodeclare copyright and license
Helmut Grohne [Tue, 11 Aug 2015 08:11:28 +0000 (10:11 +0200)]
declare copyright and license

4 years agosplit lemma-union-not-used into lemma-exchange-maps
Helmut Grohne [Thu, 2 Jul 2015 09:51:37 +0000 (11:51 +0200)]
split lemma-union-not-used into lemma-exchange-maps

New type suggested by Janis Voigtländer.

4 years agoadd example applications of bff
Helmut Grohne [Fri, 12 Jun 2015 07:45:07 +0000 (09:45 +0200)]
add example applications of bff

4 years agouse "module _" to simplify types involving Get records
Helmut Grohne [Wed, 10 Jun 2015 11:15:34 +0000 (13:15 +0200)]
use "module _" to simplify types involving Get records

4 years agodrop barred members from GetTypes
Helmut Grohne [Tue, 9 Jun 2015 14:33:31 +0000 (16:33 +0200)]
drop barred members from GetTypes

These became duplicates of their non-barred counterparts.

4 years agodrop the Function.Equality requirement from GetTypes
Helmut Grohne [Tue, 9 Jun 2015 14:09:37 +0000 (16:09 +0200)]
drop the Function.Equality requirement from GetTypes

We never used the equality property. Thus a simple function is
sufficient here. We always fulfilled the property using ≡-to-Π anyway.

4 years agorewrite lemma-disjoint-union in a more compositional way
Helmut Grohne [Wed, 3 Jun 2015 12:12:06 +0000 (14:12 +0200)]
rewrite lemma-disjoint-union in a more compositional way

4 years agoSetoidReasoning is no longer needed
Helmut Grohne [Mon, 5 Jan 2015 15:45:52 +0000 (16:45 +0100)]
SetoidReasoning is no longer needed

4 years agoturns out: ind-cong is a special case of H.cong₂
Helmut Grohne [Mon, 5 Jan 2015 09:40:23 +0000 (10:40 +0100)]
turns out: ind-cong is a special case of H.cong₂

The major differences between them are:
 * ind-cong treats the first parameter to the function implicit whereas
   H.cong₂ makes it explicit.
 * ind-cong expects a propositional proof for the first equality whereas
   H.cong₂ asks for a heterogeneous one. Lift using H.reflexive.

4 years agofix compilation against agda stdlib 0.9
Helmut Grohne [Wed, 26 Nov 2014 14:32:21 +0000 (15:32 +0100)]
fix compilation against agda stdlib 0.9

4 years agomake more parameters implicit
Helmut Grohne [Thu, 30 Oct 2014 14:05:28 +0000 (15:05 +0100)]
make more parameters implicit

All of these changes were applied to functions of type

... -> (x : ...) -> ... == x -> ...

where x could be preceded by just making the x implicit, because it can
be uniquely deduced from the equality proof.

4 years agomove all those toList calls inside _in-domain-of_
Helmut Grohne [Tue, 21 Oct 2014 09:21:41 +0000 (11:21 +0200)]
move all those toList calls inside _in-domain-of_

4 years agochange restrict and fromAscList to work with Vec
Helmut Grohne [Mon, 20 Oct 2014 15:01:38 +0000 (17:01 +0200)]
change restrict and fromAscList to work with Vec

While they do work with Lists and there is no inherent need to know the
length, they are most often invoked in a context where a Vec needs to be
converted to a List using toList. By changing them to work with Vec,
quite a few toList calls can be dropped.

5 years agogeneralize lemma-union-not-used
Helmut Grohne [Fri, 17 Oct 2014 13:36:45 +0000 (15:36 +0200)]
generalize lemma-union-not-used

5 years agosym result of lemma-lookupM-{i,checkI}nsert-other
Helmut Grohne [Thu, 16 Oct 2014 08:57:31 +0000 (10:57 +0200)]
sym result of lemma-lookupM-{i,checkI}nsert-other

Typically we have the complex term on the LHS and the simplified term on
the RHS. These lemmata did it otherwise and by symming them, we save two
syms.

5 years agoremove lemma-just≢nothing
Helmut Grohne [Wed, 15 Oct 2014 08:35:43 +0000 (10:35 +0200)]
remove lemma-just≢nothing

Special case of contradiction.

5 years agodrop the injection requirement for gl₁
Helmut Grohne [Tue, 14 Oct 2014 07:52:00 +0000 (09:52 +0200)]
drop the injection requirement for gl₁

Turns out, we never use this requirement. The only place where it may
come in relevant is the free theorems. But here non-injectivity turns
out to be reasoning about multiple get functions that are selected by
the additional index each individually satisfying the free theorem and
thus commonly satisfying it as well.

5 years agoresolve ambiguity in BFFPlug
Helmut Grohne [Fri, 26 Sep 2014 11:02:25 +0000 (13:02 +0200)]
resolve ambiguity in BFFPlug

Fixes compilation with Agda 2.4.2.

5 years agodrop-suc is cong pred
Helmut Grohne [Fri, 6 Jun 2014 07:23:00 +0000 (09:23 +0200)]
drop-suc is cong pred

5 years agofix compilation for Agda 2.3.0.1 again
Helmut Grohne [Thu, 3 Apr 2014 13:33:06 +0000 (15:33 +0200)]
fix compilation for Agda 2.3.0.1 again

It fails to infer the type of MaybeFunctor._<$>_, so give it explicitly.

5 years agoMerge branch feature-shaped into master
Helmut Grohne [Thu, 3 Apr 2014 06:57:34 +0000 (08:57 +0200)]
Merge branch feature-shaped into master

Generalizing both Vecs in the type of get to instances of Shaped. Thus allowing
trees and other data structures to be used.

5 years agodrop PartialShapeVec
Helmut Grohne [Thu, 3 Apr 2014 06:45:19 +0000 (08:45 +0200)]
drop PartialShapeVec

One can use PartialShapeShape instead, so there is limited utility for
this type. It is not used directly and there also is no PartialVecShape.

5 years agoalso allow Shaped types for the view
Helmut Grohne [Mon, 10 Mar 2014 15:11:15 +0000 (16:11 +0100)]
also allow Shaped types for the view

Albeit long, this commit is relatively boring.

5 years agogeneralize lemma-{just-sequence,sequence-successful}
Helmut Grohne [Mon, 10 Mar 2014 15:00:57 +0000 (16:00 +0100)]
generalize lemma-{just-sequence,sequence-successful}

5 years agoExample: show that PairVec is Shaped
Helmut Grohne [Mon, 10 Mar 2014 12:32:11 +0000 (13:32 +0100)]
Example: show that PairVec is Shaped

Example inspired in VoigtlaenderHMW13. Note that Vec (α × β) (length s)
is not Shaped in this way since its real index is only a number.

5 years agoport precondition to PartialShapeVec
Helmut Grohne [Mon, 10 Mar 2014 08:39:16 +0000 (09:39 +0100)]
port precondition to PartialShapeVec

5 years agoport theorem-{1,2} to PartialShapeVec
Helmut Grohne [Mon, 10 Mar 2014 08:31:57 +0000 (09:31 +0100)]
port theorem-{1,2} to PartialShapeVec

5 years agoimplement a bff on a shaped source type
Helmut Grohne [Mon, 10 Mar 2014 07:17:41 +0000 (08:17 +0100)]
implement a bff on a shaped source type

Add IsShaped and Shaped records describing shapely types as in Jay95.
Implement bff on Shaped and rewrite PartialVecVec to use the vector
shape retaining all proofs on the vector implementation.

5 years agoadd a Functor structure
Helmut Grohne [Fri, 7 Mar 2014 14:18:24 +0000 (15:18 +0100)]
add a Functor structure

The intent is to replace some uses of Vec with a structure that also
happens to be a functor. RawFunctors from the standard library provide
no laws though, so we define a Functor structure that adds the laws. As
an additional law congruence is added, because

 * Other standard library structures in Algebra.Structures also require
   congruence.
 * Otherwise the identity law would have to reason about different
   identities.

5 years agoimprove notation of theorem-1 using local bindings
Helmut Grohne [Fri, 7 Mar 2014 09:10:20 +0000 (10:10 +0100)]
improve notation of theorem-1 using local bindings

5 years agouse allFin rather than tabulate id
Helmut Grohne [Fri, 7 Mar 2014 08:16:45 +0000 (09:16 +0100)]
use allFin rather than tabulate id

5 years agoMerge branch feature-omit-sequence into master
Helmut Grohne [Wed, 5 Mar 2014 07:46:28 +0000 (08:46 +0100)]
Merge branch feature-omit-sequence into master

Beyond allowing default values during shape updates, this branch simplifies
working with shapes other than Vec.

5 years agomake lemma-sequenceV-successful more precise
Helmut Grohne [Tue, 4 Mar 2014 17:58:25 +0000 (18:58 +0100)]
make lemma-sequenceV-successful more precise

5 years agoweaken assumptions made by theorem-2 and asssoc-enough
Helmut Grohne [Wed, 26 Feb 2014 12:57:23 +0000 (13:57 +0100)]
weaken assumptions made by theorem-2 and asssoc-enough

5 years agoremove the sequenceV call from bff
Helmut Grohne [Wed, 26 Feb 2014 11:49:45 +0000 (12:49 +0100)]
remove the sequenceV call from bff

This allows bff to be more precise with regard to its failure modes,
even though we are not yet making use of that projected precision. It
allows inserting a default value for entries that could not be recovered
in a shape changing update as described in VoigtlaenderHMW13.

5 years agofix compilation on Agda 2.3.0.1
Helmut Grohne [Wed, 26 Feb 2014 09:12:50 +0000 (10:12 +0100)]
fix compilation on Agda 2.3.0.1

5 years agoconvert LiftGet module to using heterogeneous equality
Helmut Grohne [Wed, 26 Feb 2014 08:16:19 +0000 (09:16 +0100)]
convert LiftGet module to using heterogeneous equality

The reduction in proof length is impressive.

5 years agoadd intersperse as another example
Helmut Grohne [Mon, 24 Feb 2014 15:44:17 +0000 (16:44 +0100)]
add intersperse as another example

5 years agotheorem-2 works with EqR rather than SetoidReasoning again
Helmut Grohne [Mon, 24 Feb 2014 13:58:01 +0000 (14:58 +0100)]
theorem-2 works with EqR rather than SetoidReasoning again

5 years agodefine fromFunc more conveniently
Helmut Grohne [Mon, 24 Feb 2014 13:52:33 +0000 (14:52 +0100)]
define fromFunc more conveniently

5 years agogeneralize/weaken lemma-get-mapMV
Helmut Grohne [Mon, 24 Feb 2014 10:37:42 +0000 (11:37 +0100)]
generalize/weaken lemma-get-mapMV

It is now lemma-get-sequenceV and thus no longer applies the free
theorem for the function. Apart making the proof shorter, it also makes
the main use of the free theorem more visible in theorem-2.

5 years agodefine mapMV via sequenceV
Helmut Grohne [Mon, 24 Feb 2014 10:28:31 +0000 (11:28 +0100)]
define mapMV via sequenceV

This makes a few proofs easier and eliminates the need for sequence-map
entirely.

5 years agogeneralize lemma-lookupM-assoc
Helmut Grohne [Mon, 24 Feb 2014 09:38:28 +0000 (10:38 +0100)]
generalize lemma-lookupM-assoc

5 years agominor simplifications
Helmut Grohne [Fri, 21 Feb 2014 10:04:44 +0000 (11:04 +0100)]
minor simplifications

5 years agouse map-Σ to simplify lemma-mapM-successful
Helmut Grohne [Fri, 21 Feb 2014 10:04:23 +0000 (11:04 +0100)]
use map-Σ to simplify lemma-mapM-successful

5 years agofix compilation on Agda 2.3.0.1
Helmut Grohne [Mon, 17 Feb 2014 12:32:12 +0000 (13:32 +0100)]
fix compilation on Agda 2.3.0.1

5 years agouse drop, tail and take from Data.Vec in examples
Helmut Grohne [Mon, 17 Feb 2014 10:32:35 +0000 (11:32 +0100)]
use drop, tail and take from Data.Vec in examples

This is possible using the PartialVecVec implementation.

5 years agoswitch examples to PartialVecVec
Helmut Grohne [Mon, 17 Feb 2014 10:26:02 +0000 (11:26 +0100)]
switch examples to PartialVecVec

5 years agoMerge branch feature-partial-getlen into master
Helmut Grohne [Mon, 17 Feb 2014 10:04:51 +0000 (11:04 +0100)]
Merge branch feature-partial-getlen into master

It allows defining get functions that are only defined for some vector
lengths. It retains backwards compatibility with the previous state via
a VecVec compatibility module. The biggest benefit is that now standard
library functions such as tail, take and drop can be passed to bff.

Conflicts: heavy
BFF.agda (imports, bff type clash)
Bidir.agda (imports, heavy bff type clash in theorem-{1,2} and
                    lemma-get-mapMV)
Generic.agda (imports)
Precond.agda (imports, bff type clash in assoc-enough)

5 years agoavoid useless repetition
Helmut Grohne [Mon, 17 Feb 2014 09:30:43 +0000 (10:30 +0100)]
avoid useless repetition

5 years agoMerge branch feature-shape-update into master
Helmut Grohne [Fri, 14 Feb 2014 15:35:25 +0000 (16:35 +0100)]
Merge branch feature-shape-update into master

The branch enables shape updates in variety of flavours:
 * explicitly passing the desired target shape
 * providing a plugin sput : ℕ → ℕ → Maybe ℕ
 * providing a right-inverse to getlen
It also provides a backwards compatibility function to facilitate
shape-retaining updates.

5 years agoadd back original bff function before shape updates
Helmut Grohne [Fri, 14 Feb 2014 15:32:20 +0000 (16:32 +0100)]
add back original bff function before shape updates

5 years agoadd bffplug and bffinv functions and examples
Helmut Grohne [Mon, 10 Feb 2014 15:27:41 +0000 (16:27 +0100)]
add bffplug and bffinv functions and examples

We can now exploit getlen being rightinvertible and it works for drop
and sieve.

5 years agoMerge branch master into feature-shape-update
Helmut Grohne [Mon, 10 Feb 2014 14:50:27 +0000 (15:50 +0100)]
Merge branch master into feature-shape-update

For building on the sieve example.

5 years agoadd sieve to examples
Helmut Grohne [Mon, 10 Feb 2014 14:49:35 +0000 (15:49 +0100)]
add sieve to examples

5 years agoeliminate useless withs
Helmut Grohne [Fri, 7 Feb 2014 17:55:23 +0000 (18:55 +0100)]
eliminate useless withs

5 years agoreplace rewrite with cong where feasible
Helmut Grohne [Fri, 7 Feb 2014 17:32:54 +0000 (18:32 +0100)]
replace rewrite with cong where feasible

5 years agoallow shape shape updates in bff
Helmut Grohne [Fri, 7 Feb 2014 15:15:03 +0000 (16:15 +0100)]
allow shape shape updates in bff

Unlike the original version in VoigtlaenderHMW13, we do not request an
  sput : ℕ → ℕ → Maybe ℕ
function for determining the updated source shape from the original
source and updated view shape. Instead we ask the caller directly to
provide the result of sput together with a proof that its getlen matches
with the provided, updated view.

The precondition assoc-enough is not enriched in this way and still
requires a non-changing shape. I.e. it says what it said before.

5 years agobe more precise about which lookups we use
Helmut Grohne [Wed, 5 Feb 2014 14:59:06 +0000 (15:59 +0100)]
be more precise about which lookups we use

5 years agostrip even more implementation detail in Precond
Helmut Grohne [Wed, 5 Feb 2014 14:54:54 +0000 (15:54 +0100)]
strip even more implementation detail in Precond

5 years agostrip implementation detail from lemma-union-delete-fromFunc
Helmut Grohne [Wed, 5 Feb 2014 14:47:05 +0000 (15:47 +0100)]
strip implementation detail from lemma-union-delete-fromFunc

5 years agoadd lemma-lookupM-fromFunc
Helmut Grohne [Wed, 5 Feb 2014 14:21:57 +0000 (15:21 +0100)]
add lemma-lookupM-fromFunc

The new lemma replaces two uses of lemma-fromFunc-tabulate, because the
latter exposes the implementation of FinMapMaybe, whereas the former
argues about the behaviour of FinMapMaybe. The aim of not exposing the
implementation (apart from brevity) is to enable refactoring.

5 years agoadd examples
Helmut Grohne [Wed, 5 Feb 2014 10:05:29 +0000 (11:05 +0100)]
add examples

5 years agoremove unused imports
Helmut Grohne [Tue, 4 Feb 2014 10:12:42 +0000 (11:12 +0100)]
remove unused imports

Most of the became unused by using the convenience functions introduced
in the parent commit.

5 years agoadd convenience members to PartialVecVec.Get
Helmut Grohne [Tue, 4 Feb 2014 09:52:49 +0000 (10:52 +0100)]
add convenience members to PartialVecVec.Get

5 years agoMerge branch feature-get-record into feature-partial-getlen
Helmut Grohne [Tue, 4 Feb 2014 09:32:34 +0000 (10:32 +0100)]
Merge branch feature-get-record into feature-partial-getlen

These two features heavily interconnect. As such it makes sense to
integrate them properly. This non-trivial merge does that work. Compared
to feature-partial-getlen a few definitions moved from FreeTheorems.agda
to GetTypes.agda. Many types changed compared to both branches.

Conflicts:
BFF.agda
Bidir.agda
FreeTheorems.agda
Precond.agda
        conflict in GetTypes.agda not detected by merge

5 years agomake things compile with 2.3.0.1
Helmut Grohne [Mon, 3 Feb 2014 15:36:11 +0000 (16:36 +0100)]
make things compile with 2.3.0.1

 * Remove let patter , match = foo usage
 * Remove Qualified.infix-symbol usage
 * Add non-obvious absurd patterns
 * Qualify constructors

5 years agoMerge branch feature-get-record into master
Helmut Grohne [Mon, 3 Feb 2014 13:51:06 +0000 (14:51 +0100)]
Merge branch feature-get-record into master

This branch brings three main benefits:
 * Only one explicit parameter is needed to ask for a get function.
 * The postulated free theorems are mostly turned into preconditions,
   i.e. the only use of the postulates is in LiftGet.
 * We can now convert list based get functions to vec based ones and back
   including the (now) accompanying free theorem.

5 years agoalso show the other direction GetL-to-GetV
Helmut Grohne [Mon, 3 Feb 2014 13:41:19 +0000 (14:41 +0100)]
also show the other direction GetL-to-GetV

5 years agoadd a GetV-to-GetL transformer
Helmut Grohne [Mon, 3 Feb 2014 10:41:14 +0000 (11:41 +0100)]
add a GetV-to-GetL transformer

This is an improved version of getVec-to-getList in that it also
transports the corresponding free theorem.

5 years agofully allow partial get functions
Helmut Grohne [Thu, 30 Jan 2014 13:23:10 +0000 (14:23 +0100)]
fully allow partial get functions

By choosing gl₁ = suc and gl₂ = id, the tail function can now be
bidirectionalized.

5 years agomake the getlen functions explicit in PartialVecBFF
Helmut Grohne [Thu, 30 Jan 2014 13:04:29 +0000 (14:04 +0100)]
make the getlen functions explicit in PartialVecBFF

There is no way for Agda to infer these functions or even the intended
index Setoid, so making these explicit is rather required.

5 years agoexpress VecBFF via PartialVecBFF
Helmut Grohne [Thu, 30 Jan 2014 13:01:10 +0000 (14:01 +0100)]
express VecBFF via PartialVecBFF

5 years agoallow importing of Bidir without any postulates
Helmut Grohne [Thu, 30 Jan 2014 08:13:11 +0000 (09:13 +0100)]
allow importing of Bidir without any postulates

5 years agopass get functions as records
Helmut Grohne [Thu, 30 Jan 2014 08:02:06 +0000 (09:02 +0100)]
pass get functions as records

This allows passing both getlen and get as a single parameter. It also
allows to make the free theorem a prerequisite instead of a postulate.

5 years agosimplify compilation of the whole source
Helmut Grohne [Thu, 30 Jan 2014 07:07:29 +0000 (08:07 +0100)]
simplify compilation of the whole source

5 years agodefine bff on a partial getlen
Helmut Grohne [Tue, 28 Jan 2014 14:15:12 +0000 (15:15 +0100)]
define bff on a partial getlen

The representation chosen is to give both an injection gl₁ and a
function gl₂ (formerly getlen), such that by choosing a non-identity for
gl₁ partiality of getlen can be expressed. An alternative would have
been to allow getlen to return a Maybe ℕ and have get return
  maybe (Vec A) ⊤ (getlen n)
thus sending all inputs for which getlen yields nothing to tt. It seems
that while there is no way to obtain a such a getlen predicate from an
arbitrary index Setoid I, it should be possible to manufacture a Setoid
from a predicate. Thanks to Stefan Mehner for the insightful discussion.

5 years agoimprove readability using _∋_≈_ instead of Setoid._≈_
Helmut Grohne [Tue, 28 Jan 2014 09:53:45 +0000 (10:53 +0100)]
improve readability using _∋_≈_ instead of Setoid._≈_

5 years agothere is no need to work with IsPreorder
Helmut Grohne [Tue, 28 Jan 2014 08:36:54 +0000 (09:36 +0100)]
there is no need to work with IsPreorder

5 years agouse the indexed version of the Vec Setoid
Helmut Grohne [Tue, 28 Jan 2014 08:30:45 +0000 (09:30 +0100)]
use the indexed version of the Vec Setoid

5 years agocleanup unused function and import
Helmut Grohne [Tue, 28 Jan 2014 08:16:26 +0000 (09:16 +0100)]
cleanup unused function and import

5 years agoMerge branch feature-delete
Helmut Grohne [Mon, 27 Jan 2014 12:46:47 +0000 (13:46 +0100)]
Merge branch feature-delete

Most conflicts stem from varying imports or added functions and a
take-both approach merges them. A notable exception is theorem-2, where
a new result sequence-cong was required. Apart from that, theorem-2
could be taken almost verbatim from feature-delete albeit its type
coming from feature-decsetoid.

Conflicts:
Bidir.agda
FinMap.agda
Generic.agda
Precond.agda

5 years agoMerge branch feature-decsetoid
Helmut Grohne [Mon, 27 Jan 2014 09:50:15 +0000 (10:50 +0100)]
Merge branch feature-decsetoid

5 years agocleanup unused functions and useless steps
Helmut Grohne [Mon, 27 Jan 2014 08:31:56 +0000 (09:31 +0100)]
cleanup unused functions and useless steps