Commit 2022-04-28 15:22 7778d96d

feat: slim check (#254) An absolute minimal port of Lean 3's slim_check, not featuring stuff like subtypes, existential quantifiers etc. But the basic infrastructure to set all of this up and some basic instances already as well. The PhantomFunction was introduced to avoid noncomputable instances since SizeOf is not computable but we need to store it as a field in SampleableExt so we work around this by defining a PhantomFunction which is guaranteed to be eliminated by the compiler during code generation. I do however believe that this is not the right file for it to live in?