projects
/
~helmut
/
bidiragda.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
~helmut/bidiragda.git
2020-08-01
Helmut Grohne
move imports for agda-stdlib 1.3
master
commit
|
commitdiff
|
tree
|
snapshot
2020-08-01
Helmut Grohne
individually open ≡-Reasoning
commit
|
commitdiff
|
tree
|
snapshot
2019-09-29
Helmut Grohne
port to agda/2.6.0.1 and agda-stdlib/1.1
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
Generic.toList-fromList is Data.Vec.Properties.toList...
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
Generic.just-injective is Data.Maybe.just-injective
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
FinMap.lemma-lookupM-delete is another variant of Data...
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
FinMap.lemma-lookupM-fromFunc is almost Data.Vec.Proper...
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
FinMap.lemma-tabulate-∘ is also known as Data.Vec.Prope...
commit
|
commitdiff
|
tree
|
snapshot
2019-03-31
Helmut Grohne
replace FinMap.lemma-lookupM-empty with Data.Vec.Proper...
commit
|
commitdiff
|
tree
|
snapshot
2018-11-25
Helmut Grohne
port to agda/2.5.4.1 and agda-stdlib/0.17
commit
|
commitdiff
|
tree
|
snapshot
2018-11-25
Helmut Grohne
remove unused imports
commit
|
commitdiff
|
tree
|
snapshot
2018-11-25
Helmut Grohne
make the setoid parameter to sequenceV-cong explicit
commit
|
commitdiff
|
tree
|
snapshot
2018-11-25
Helmut Grohne
reorganize equality imports
commit
|
commitdiff
|
tree
|
snapshot
2018-11-25
Helmut Grohne
fix missing import of "length"
commit
|
commitdiff
|
tree
|
snapshot
2018-01-02
Helmut Grohne
length-replicate is now upstream as well
commit
|
commitdiff
|
tree
|
snapshot
2018-01-02
Helmut Grohne
remove lemma-lookupM-insert-other in favour of lookup...
commit
|
commitdiff
|
tree
|
snapshot
2018-01-02
Helmut Grohne
remove lemma-lookupM-insert in favour of lookup∘update
commit
|
commitdiff
|
tree
|
snapshot
2018-01-01
Helmut Grohne
fix compilation with agda 2.5.3, agda-stdlib 0.14
commit
|
commitdiff
|
tree
|
snapshot
2016-06-21
Helmut Grohne
fix compilation with agda 2.5.1, agda-stdlib 0.12
commit
|
commitdiff
|
tree
|
snapshot
2015-08-11
Helmut Grohne
declare copyright and license
commit
|
commitdiff
|
tree
|
snapshot
2015-07-02
Helmut Grohne
split lemma-union-not-used into lemma-exchange-maps
commit
|
commitdiff
|
tree
|
snapshot
2015-06-12
Helmut Grohne
add example applications of bff
commit
|
commitdiff
|
tree
|
snapshot
2015-06-10
Helmut Grohne
use "module _" to simplify types involving Get records
commit
|
commitdiff
|
tree
|
snapshot
2015-06-09
Helmut Grohne
drop barred members from GetTypes
commit
|
commitdiff
|
tree
|
snapshot
2015-06-09
Helmut Grohne
drop the Function.Equality requirement from GetTypes
commit
|
commitdiff
|
tree
|
snapshot
2015-06-03
Helmut Grohne
rewrite lemma-disjoint-union in a more compositional way
commit
|
commitdiff
|
tree
|
snapshot
2015-01-05
Helmut Grohne
SetoidReasoning is no longer needed
commit
|
commitdiff
|
tree
|
snapshot
2015-01-05
Helmut Grohne
turns out: ind-cong is a special case of H.cong₂
commit
|
commitdiff
|
tree
|
snapshot
2014-11-26
Helmut Grohne
fix compilation against agda stdlib 0.9
commit
|
commitdiff
|
tree
|
snapshot
2014-10-30
Helmut Grohne
make more parameters implicit
commit
|
commitdiff
|
tree
|
snapshot
2014-10-21
Helmut Grohne
move all those toList calls inside _in-domain-of_
commit
|
commitdiff
|
tree
|
snapshot
2014-10-20
Helmut Grohne
change restrict and fromAscList to work with Vec
commit
|
commitdiff
|
tree
|
snapshot
2014-10-17
Helmut Grohne
generalize lemma-union-not-used
commit
|
commitdiff
|
tree
|
snapshot
2014-10-16
Helmut Grohne
sym result of lemma-lookupM-{i,checkI}nsert-other
commit
|
commitdiff
|
tree
|
snapshot
2014-10-15
Helmut Grohne
remove lemma-just≢nothing
commit
|
commitdiff
|
tree
|
snapshot
2014-10-14
Helmut Grohne
drop the injection requirement for gl₁
commit
|
commitdiff
|
tree
|
snapshot
2014-09-26
Helmut Grohne
resolve ambiguity in BFFPlug
commit
|
commitdiff
|
tree
|
snapshot
2014-06-06
Helmut Grohne
drop-suc is cong pred
commit
|
commitdiff
|
tree
|
snapshot
2014-04-03
Helmut Grohne
fix compilation for Agda 2.3.0.1 again
commit
|
commitdiff
|
tree
|
snapshot
2014-04-03
Helmut Grohne
Merge branch feature-shaped into master
commit
|
commitdiff
|
tree
|
snapshot
2014-04-03
Helmut Grohne
drop PartialShapeVec
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
also allow Shaped types for the view
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
generalize lemma-{just-sequence,sequence-successful}
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
Example: show that PairVec is Shaped
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
port precondition to PartialShapeVec
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
port theorem-{1,2} to PartialShapeVec
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Helmut Grohne
implement a bff on a shaped source type
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Helmut Grohne
add a Functor structure
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Helmut Grohne
improve notation of theorem-1 using local bindings
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Helmut Grohne
use allFin rather than tabulate id
commit
|
commitdiff
|
tree
|
snapshot
2014-03-05
Helmut Grohne
Merge branch feature-omit-sequence into master
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Helmut Grohne
make lemma-sequenceV-successful more precise
commit
|
commitdiff
|
tree
|
snapshot
2014-02-26
Helmut Grohne
weaken assumptions made by theorem-2 and asssoc-enough
commit
|
commitdiff
|
tree
|
snapshot
2014-02-26
Helmut Grohne
remove the sequenceV call from bff
commit
|
commitdiff
|
tree
|
snapshot
2014-02-26
Helmut Grohne
fix compilation on Agda 2.3.0.1
commit
|
commitdiff
|
tree
|
snapshot
2014-02-26
Helmut Grohne
convert LiftGet module to using heterogeneous equality
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
add intersperse as another example
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
theorem-2 works with EqR rather than SetoidReasoning...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
define fromFunc more conveniently
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
generalize/weaken lemma-get-mapMV
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
define mapMV via sequenceV
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Helmut Grohne
generalize lemma-lookupM-assoc
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Helmut Grohne
minor simplifications
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Helmut Grohne
use map-Σ to simplify lemma-mapM-successful
commit
|
commitdiff
|
tree
|
snapshot
2014-02-17
Helmut Grohne
fix compilation on Agda 2.3.0.1
commit
|
commitdiff
|
tree
|
snapshot
2014-02-17
Helmut Grohne
use drop, tail and take from Data.Vec in examples
commit
|
commitdiff
|
tree
|
snapshot
2014-02-17
Helmut Grohne
switch examples to PartialVecVec
commit
|
commitdiff
|
tree
|
snapshot
2014-02-17
Helmut Grohne
Merge branch feature-partial-getlen into master
commit
|
commitdiff
|
tree
|
snapshot
2014-02-17
Helmut Grohne
avoid useless repetition
commit
|
commitdiff
|
tree
|
snapshot
2014-02-14
Helmut Grohne
Merge branch feature-shape-update into master
commit
|
commitdiff
|
tree
|
snapshot
2014-02-14
Helmut Grohne
add back original bff function before shape updates
commit
|
commitdiff
|
tree
|
snapshot
2014-02-10
Helmut Grohne
add bffplug and bffinv functions and examples
commit
|
commitdiff
|
tree
|
snapshot
2014-02-10
Helmut Grohne
Merge branch master into feature-shape-update
commit
|
commitdiff
|
tree
|
snapshot
2014-02-10
Helmut Grohne
add sieve to examples
commit
|
commitdiff
|
tree
|
snapshot
2014-02-07
Helmut Grohne
eliminate useless withs
commit
|
commitdiff
|
tree
|
snapshot
2014-02-07
Helmut Grohne
replace rewrite with cong where feasible
commit
|
commitdiff
|
tree
|
snapshot
2014-02-07
Helmut Grohne
allow shape shape updates in bff
commit
|
commitdiff
|
tree
|
snapshot
2014-02-05
Helmut Grohne
be more precise about which lookups we use
commit
|
commitdiff
|
tree
|
snapshot
2014-02-05
Helmut Grohne
strip even more implementation detail in Precond
commit
|
commitdiff
|
tree
|
snapshot
2014-02-05
Helmut Grohne
strip implementation detail from lemma-union-delete...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-05
Helmut Grohne
add lemma-lookupM-fromFunc
commit
|
commitdiff
|
tree
|
snapshot
2014-02-05
Helmut Grohne
add examples
commit
|
commitdiff
|
tree
|
snapshot
2014-02-04
Helmut Grohne
remove unused imports
commit
|
commitdiff
|
tree
|
snapshot
2014-02-04
Helmut Grohne
add convenience members to PartialVecVec.Get
commit
|
commitdiff
|
tree
|
snapshot
2014-02-04
Helmut Grohne
Merge branch feature-get-record into feature-partial...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Helmut Grohne
make things compile with 2.3.0.1
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Helmut Grohne
Merge branch feature-get-record into master
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Helmut Grohne
also show the other direction GetL-to-GetV
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Helmut Grohne
add a GetV-to-GetL transformer
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
fully allow partial get functions
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
make the getlen functions explicit in PartialVecBFF
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
express VecBFF via PartialVecBFF
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
allow importing of Bidir without any postulates
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
pass get functions as records
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Helmut Grohne
simplify compilation of the whole source
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Helmut Grohne
define bff on a partial getlen
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Helmut Grohne
improve readability using _∋_≈_ instead of Setoid._≈_
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Helmut Grohne
there is no need to work with IsPreorder
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Helmut Grohne
use the indexed version of the Vec Setoid
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Helmut Grohne
cleanup unused function and import
commit
|
commitdiff
|
tree
|
snapshot
next