~helmut/bidiragda.git - Bidirectionalization for Free in Agda (http://subdivi.de/~helmut/academia/fsbxia.pdf)

Age	Commit message (Expand)	Author
2012-09-26	use _\==n_ and _\notin_ instead of \neg	Helmut Grohne
2012-09-26	rename suc-\== to suc-injective	Helmut Grohne
2012-09-26	import [_] instead of Reveal_is_	Helmut Grohne
2012-09-18	Merge branch 'using-vec'	Helmut Grohne
2012-09-18	one more application of lemma-just\==nnothing	Helmut Grohne
2012-09-17	save a with in lemma-\inn-lookupM-assoc	Helmut Grohne
2012-09-14	employ rewrite in lemma-map-lookupM-assoc	Helmut Grohne
2012-09-14	\::-subst is a special case of subst-cong	Helmut Grohne
2012-09-14	vec-len-via-list and length-toList are the same	Helmut Grohne
2012-09-14	complete missing parts of LiftGet	Helmut Grohne
2012-09-11	show fromList-toList in the subst form	Helmut Grohne
2012-09-11	LiftGet: replace vec-length-same with toList-subst	Helmut Grohne
2012-09-10	LiftGet: vec-length is also known as subst (Vec A)	Helmut Grohne
2012-09-08	give a sufficient precondition for theorem-2	Helmut Grohne
2012-09-04	rewrite main theorems to using Vec instead of List	Helmut Grohne
2012-09-04	formulate List <-> Vec isomorphism problems	Helmut Grohne
2012-08-30	prove LiftGet.get-trafo-2-getlen	Helmut Grohne
2012-08-30	phrase other half of bijection in LiftGet	Helmut Grohne
2012-08-30	prove half of the bijection in LiftGet	Helmut Grohne
2012-08-30	give the type of different gets a name	Helmut Grohne
2012-08-06	attempt isomorphism between get on List and on Vec	Helmut Grohne
2012-06-19	third definition of bff	Helmut Grohne
2012-06-05	make the Vec bff more similar to the List version	Helmut Grohne
2012-06-05	define a bff over Vec	Helmut Grohne
2012-06-05	move bff and friends to submodule ListBFF	Helmut Grohne
2012-06-05	move checkInsert and related properties to CheckInsert.agda	Helmut Grohne
2012-04-27	lemma-2: do not confuse lookup with lookupM	Helmut Grohne
2012-04-27	use fromFunc to define union	Helmut Grohne
2012-04-27	prove the theorem-2	Helmut Grohne
2012-04-20	remove lemma-\in-lookupM-assoc	Helmut Grohne
2012-04-20	complete lemma-2 using new property _in-domain-of_	Helmut Grohne
2012-04-19	reduce hole in lemma-2	Helmut Grohne
2012-04-19	FinMap: lemma-lookupM-restrict drop useless implicit	Helmut Grohne
2012-04-19	move lemma-just!=nothing to FinMap and use it there	Helmut Grohne
2012-04-17	inline bot-elim into lemma-just-nothing	Helmut Grohne
2012-04-04	abstract proofs over checkInsert	Helmut Grohne
2012-03-16	fix wrong function name in lemma-2	Helmut Grohne
2012-02-09	remove useless braces	Helmut Grohne
2012-02-09	avoid a sym in lemma-union-restrict	Helmut Grohne
2012-02-09	s/generate/restrict/g	Helmut Grohne
2012-02-09	rephrase free-theorem-list-list using pointwise equality	Helmut Grohne
2012-02-09	formulate theorem-2	Helmut Grohne
2012-02-09	prove lemma-union-generate	Helmut Grohne
2012-02-09	prove theorem-1 assuming a lemma-union-generate	Helmut Grohne
2012-02-09	started proving theorem-1	Helmut Grohne
2012-02-09	introduce denumerate	Helmut Grohne
2012-01-31	replace idrange with enumerate	Helmut Grohne
2012-01-31	postulate free theorem for List a -> List a	Helmut Grohne
2012-01-26	recursion of lemma-2	Helmut Grohne
2012-01-26	started proving lemma-2	Helmut Grohne