feat: Extract type error and new constants #128

Merged

aniva merged 17 commits from frontend/infotree into dev

2024-12-11 01:25:36 -08:00

Author	SHA1	Message	Date
Leni Aniva	7cba8efd54	Merge branch 'dev' into frontend/infotree	2024-12-11 01:14:15 -08:00
Leni Aniva	95503c45e4	doc: frontend.process newConstants	2024-12-10 21:45:57 -08:00
Leni Aniva	681c3fb78d	fix: Disallow indeterminant type `sorry`	2024-12-10 12:21:56 -08:00
Leni Aniva	37a5884be4	fix: Use `ppSyntax` instead of `ppTactic`	2024-12-09 21:39:33 -08:00
Leni Aniva	1527743900	refactor: Optionalize CompilationUnit	2024-12-09 21:00:33 -08:00
Leni Aniva	eb0374dfb3	feat: Collect new constants in repl	2024-12-09 20:57:25 -08:00
Leni Aniva	9a69c48cb2	fix: Integration test failure	2024-12-09 20:42:05 -08:00
Leni Aniva	dd00d803d1	feat: Collect sorry/elab failure boundaries	2024-12-09 20:38:27 -08:00
Leni Aniva	0b4ded1049	fix: Collect sorrys and type mismatches	2024-12-09 20:15:53 -08:00
Leni Aniva	5ef2b5c118	feat: Collect newly defined constants	2024-12-09 19:40:00 -08:00
Leni Aniva	2d068ecd50	fix: Use guarded `isDefEq`	2024-12-09 00:06:20 -08:00
Leni Aniva	17ab2eafd8	fix: Halt on match guard	2024-12-09 00:03:53 -08:00
Leni Aniva	ea813e5bc5	feat: Monadic info collection	2024-12-08 23:21:36 -08:00
Leni Aniva	b950dc9b1a	fix: Verbose printing of infotree	2024-12-08 22:51:55 -08:00
Leni Aniva	9ede3cf717	feat: InfoTree printing	2024-12-08 15:38:03 -08:00
Leni Aniva	4de53e0547	Merge branch 'dev' into frontend/infotree	2024-12-08 12:54:19 -08:00
Leni Aniva	9894ad7c7e	refactor: InfoTree functions	2024-11-26 12:16:14 -08:00