Dylan Ede
Dylan Ede
@kvark A lot of the code in the example is probably analogous to existing code in gfx_text. Stuff like keeping track of which glyphs to draw, producing the quads to...
Is there anything more I can do to help diagnose this problem?
Naïve question here: what would be wrong with `intro {expr}` translating to WhyML equivalent to the "hacky" solution, with preconditions on the generated lemma function that match all preconditions and...
Just bumped into this problem. Anyone got a workaround?
`Type*` is a macro from mathlib that introduces a fresh anonymous universe level parameter for each variable, so `(α β : Type*)` is equivalent to `(α : Type u) (β...
What I'm trying to do is come up with a safe abstraction for accessing pointers (= converting to references) to data you can prove you have a borrow for and...
Regarding notation, it is a shame that do-notation desugaring in Lean is not defined the same way as in Agda, where it is defined in terms of free functions rather...
I think actually that just including the `Sized T` parameter everywhere would be clumsy, and also does not solve the problem of not being able to reason about other properties...