Juneyoung Lee 4b739dd6e4 Add more comments and fix broken proofs		2023-07-14 20:12:48 +00:00
..
spec	Add more comments and fix broken proofs	2023-07-14 20:12:48 +00:00
bitvector.lean	Reduce the size of proof	2019-02-08 07:41:22 +09:00
common.lean	add copyright banner	2018-05-17 09:36:47 +01:00
freevar.lean	Add more comments and fix broken proofs	2023-07-14 20:12:48 +00:00
irsem.lean	Rename bigstep_exe/step_exe to bigstep/step	2019-02-08 07:40:45 +09:00
irsem_exec.lean	Implement irtest_run	2019-02-08 07:38:33 +09:00
irsem_smt.lean	add copyright banner	2018-05-17 09:36:47 +01:00
irtest_run.lean	Add canonicalization of free variable types	2019-02-08 07:41:26 +09:00
irtype.lean	add copyright banner	2018-05-17 09:36:47 +01:00
lang.lean	Add simp to bop_isdiv, add a simple lemma	2019-02-08 07:38:50 +09:00
lang_tostr.lean	Implement irtest_run	2019-02-08 07:38:33 +09:00
langparser.lean	add copyright banner	2018-05-17 09:36:47 +01:00
main.lean	Minor fix	2019-02-08 07:40:57 +09:00
ops.lean	add copyright banner	2018-05-17 09:36:47 +01:00
proptest.lean	Add canonicalization of free variable types	2019-02-08 07:41:26 +09:00
proptest_run.lean	Add more comments and fix broken proofs	2023-07-14 20:12:48 +00:00
smtcompile.lean	add copyright banner	2018-05-17 09:36:47 +01:00
smtexpr.lean	Add more comments and fix broken proofs	2023-07-14 20:12:48 +00:00
vcgen.lean	add copyright banner	2018-05-17 09:36:47 +01:00
verifyopt.lean	Remove TODOs, address the concerns at appropriate places	2019-02-08 07:52:51 +09:00