git.ak3n.com - cubicaltt.git/shortlog

2015-04-20	Anders Mörtberg	Fix printing of VPi	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders Mörtberg	Fix retract	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders	Make normal print nicer names	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders	Fix printing of @	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders	Add quotient example	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders	Split higherhit into multiple files	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders	Merge remote-tracking branch 'origin/higherhits'	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders Mörtberg	Fix the way @ binds (it is now like normal application)	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders Mörtberg	Fix a TODO in the resolver (the arguments in a path...	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders Mörtberg	Fix all the old examples of HITs	commit \| commitdiff \| tree \| snapshot
2015-04-20	Anders Mörtberg	Remove the @ in PLabel	commit \| commitdiff \| tree \| snapshot
2015-04-19	coquand	any isomorphism is an equivalence	commit \| commitdiff \| tree \| snapshot
2015-04-19	coquand	if A and B are isomorphic, set A -> set B, normal form	commit \| commitdiff \| tree \| snapshot
2015-04-19	coquand	if A and B are isomorphic, prop A -> prop B, normal...	commit \| commitdiff \| tree \| snapshot
2015-04-19	coquand	result on equivalence of fibers	commit \| commitdiff \| tree \| snapshot
2015-04-19	coquand	new proof of Hedberg's theorem	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	some examples	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	lookName error msg for debugging	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	bugfix in PBranches	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	let the system in a pcon know about all pcons in the sum	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	bugfix	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	bugfix in resolver	commit \| commitdiff \| tree \| snapshot
2015-04-18	Simon Huber	wip (not working yet)	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders	Fix printing of goals and environments (TODO: Fix ...	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders	Rewrite app and support using case-of	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders	Use Except instead or Error	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders	Remove tabs	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders Mörtberg	Only show second part of VPi x (VLam ...)	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders Mörtberg	Also normalize the type of lambdas and print VPi nicer	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders Mörtberg	Use showTer1 to print closures	commit \| commitdiff \| tree \| snapshot
2015-04-17	Anders Mörtberg	Fix uafunext2	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders	Remove some incidentally commited holes	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders	Reintroduce _ in identifier again	commit \| commitdiff \| tree \| snapshot
2015-04-16	Simon Huber	reintroduce nicer mkVar	commit \| commitdiff \| tree \| snapshot
2015-04-16	Simon Huber	keep name if we have it when generating a fresh name	commit \| commitdiff \| tree \| snapshot
2015-04-16	Simon Huber	change mkVar back to how it was	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Add indentation to Checking and start changing mkVar...	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Only print File loaded if file type checks	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Change gensym	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Make holes print the context	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Trailing whitespace	commit \| commitdiff \| tree \| snapshot
2015-04-16	Anders Mörtberg	Fix undefined	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders	Finish example of integers as a HIT	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders	Remove some code from ex1	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders	Fix bug in type checker for HITs	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders	Fix undefined	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders Mörtberg	Remove VUndef	commit \| commitdiff \| tree \| snapshot
2015-04-15	Anders Mörtberg	Add very simple support for holes	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders Mörtberg	Make list compile	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders Mörtberg	Make undefined only occur as a declaration so that...	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders Mörtberg	Undef is neutral (but there is an issue with inferType...	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders Mörtberg	Start defining integers as a HIT and proving that they...	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders	Fix printing of fst, snd and lambdas	commit \| commitdiff \| tree \| snapshot
2015-04-14	Anders	Update the description in demo.ctt	commit \| commitdiff \| tree \| snapshot
2015-04-14	coquand	added some lines in ex1.ctt	commit \| commitdiff \| tree \| snapshot
2015-04-14	coquand	added some lines in ex1.ctt	commit \| commitdiff \| tree \| snapshot
2015-04-14	coquand	small change in helix.ctt	commit \| commitdiff \| tree \| snapshot
2015-04-14	coquand	one example with constant functions	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders Mörtberg	Fix bug in Resolver	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders Mörtberg	Remove contr from equiv	commit \| commitdiff \| tree \| snapshot
2015-04-13	Simon Huber	license should include names	commit \| commitdiff \| tree \| snapshot
2015-04-13	coquand	small modification in the file susp	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders Mörtberg	Update help message	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders Mörtberg	Update README	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders Mörtberg	Move stream to experiments	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Add dependency graph script	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Update README	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Lots of cleaning in the examples	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Add equiv and uafunext2	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Reorganized and cleaned some examples	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Update README	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Fix README	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Update README	commit \| commitdiff \| tree \| snapshot
2015-04-13	Anders	Update the README and examples	commit \| commitdiff \| tree \| snapshot
2015-04-13	Simon Huber	demo from the proglog talk	commit \| commitdiff \| tree \| snapshot
2015-04-13	Simon Huber	use smart fst/snd in act	commit \| commitdiff \| tree \| snapshot
2015-04-12	Simon Huber	added thierrys examples (funext from univalence,helix)	commit \| commitdiff \| tree \| snapshot
2015-04-11	Simon Huber	fixing use of isNeutral	commit \| commitdiff \| tree \| snapshot
2015-04-10	Anders	Fix parsing of trans, comp, etc.	commit \| commitdiff \| tree \| snapshot
2015-04-10	Anders	Explicitly pass around the history	commit \| commitdiff \| tree \| snapshot
2015-04-10	mortberg	Merge pull request #6 from nad/master	commit \| commitdiff \| tree \| snapshot
2015-04-09	Anders Mörtberg	Start the proof that ua implies funext	commit \| commitdiff \| tree \| snapshot
2015-04-09	Nils Anders...	Proved (?) that equality coincides with bisimilarity.	commit \| commitdiff \| tree \| snapshot
2015-04-09	Anders	Clean examples	commit \| commitdiff \| tree \| snapshot
2015-04-09	Anders	Add normalization function	commit \| commitdiff \| tree \| snapshot
2015-04-09	Simon Huber	funext from interval	commit \| commitdiff \| tree \| snapshot
2015-04-08	Simon Huber	don't crash the main loop if error in eval	commit \| commitdiff \| tree \| snapshot
2015-04-08	Simon Huber	split annotation is now the type not the family; typo...	commit \| commitdiff \| tree \| snapshot
2015-04-08	Simon Huber	evaluate undefined into a closure	commit \| commitdiff \| tree \| snapshot
2015-04-08	Simon Huber	function should be known in def (for general recursion)	commit \| commitdiff \| tree \| snapshot
2015-04-08	Anders	Cleaning	commit \| commitdiff \| tree \| snapshot
2015-04-08	Simon Huber	added thierrys adapted files	commit \| commitdiff \| tree \| snapshot
2015-04-07	Simon Huber	improve show of a sum	commit \| commitdiff \| tree \| snapshot
2015-04-07	Simon Huber	analogous fix for pathUniv	commit \| commitdiff \| tree \| snapshot
2015-04-07	Simon Huber	bugfix in pathUnivTrans	commit \| commitdiff \| tree \| snapshot
2015-03-31	Simon Huber	reintroduce faceEnv	commit \| commitdiff \| tree \| snapshot
2015-03-31	Anders	Cleaned and simplified type checker	commit \| commitdiff \| tree \| snapshot
2015-03-30	Simon Huber	bugfix in simplify, conv; extended prelude	commit \| commitdiff \| tree \| snapshot
2015-03-29	Anders	Fix parsing of /\	commit \| commitdiff \| tree \| snapshot
2015-03-29	Anders Mörtberg	Fix error message when path constructors are written...	commit \| commitdiff \| tree \| snapshot
next

My fork of cubicaltt with web interface using Reflex.

RSS Atom