makkai - Type theory implementation

Age	Commit message (Collapse)	Author
2026-05-06	fixing ...	tslil

2026-05-06	WiP	tslil

2026-05-05	address remaining TODO, fix issues with left-nesting for for and ext, add ↵	tslil
	motivation blurb to the readme
2026-05-05	replace todo! with real errors	tslil

2026-05-01	working on fixing app, rework ast to have generics etc	tslil

2026-05-01	make parser more lenient, add the one simplex example, fix naming for records	tslil

2026-04-30	wip case for instances	tslil

2026-04-30	fill in some more todos	tslil

2026-04-30	lost track of what's going on	tslil

2026-04-29	switch to references in many places for check_*, complete logic of Var case ↵	tslil
	for App
2026-04-29	implement canonicalisation in case arms, work through first bit of app	tslil

2026-04-28	snapshot of working through instances/singatures <> sets/elements	tslil

2026-04-28	rework checking logic to revolve around "stuck" computations, the meaning of ↵	tslil
	Hypothetical is now reserved for formal bindings
2026-04-27	prepare for more work on signatures, in particular this means processing ↵	tslil
	records in telescoped contexts rework ElementValue, CheckedElement to be type aliases for the generic version over Term : Type
2026-04-27	basic signature functionality, missing extension signatures	tslil

2026-04-27	refactor equality checking and fields as we start to build towards signatures	tslil

2026-04-27	report _which_ element does not belong to the correct set, at the bottom of ↵	tslil
	the tree anyway
2026-04-27	enforce arm match uniqueness again	tslil

2026-04-27	add distinction between hypothetical and concrete elements to the set ↵	tslil
	checker, it now enforces that all arms in case are well typed!
2026-04-27	refactor error to be clearer	tslil

2026-04-24	computing cases	tslil