Hoist simple lemmas and theorems

CakeML / pure

A verified compiler for a lazy functional language

Other

32 stars 4 forks source link

Hoist simple lemmas and theorems #36

Open hrutvik opened 1 year ago

hrutvik commented 1 year ago

We have lots of simple helper theorems scattered everywhere. We should move as many as possible to pure_misc, and clearly mark ones that are candidates for porting to HOL.