6 commits

Author	SHA1	Message	Date
Yiyun Liu	96ad0a4740	Add stub for the new coqleq_complete'	2025-03-11 00:14:43 -04:00
Yiyun Liu	849d19708e	Add new definition of algo_dom	2025-03-10 14:30:36 -04:00
Yiyun Liu	437c97455e	Finish the soundness and completeness proof of the subtyping algorithm	2025-03-06 20:42:08 -05:00
Yiyun Liu	6f154cc9c6	Add stub for check_sub	2025-03-06 16:20:32 -05:00
Yiyun Liu	96b3139726	Prove termination	2025-03-06 15:39:27 -05:00
Yiyun Liu	b29d567ef0	Add termination	2025-03-05 00:18:28 -05:00