Pedro Abreu
Pedro Abreu
A follow up question to this is how does coq figures out the decreasing argument here
We will deal with this by hard coding the necessary induction principles for now. Apparently cedille folks will make this coercion implicit later on.
As an example, consider the translation of eqb ``` eqb : Π n : nat . Π m : nat . bool = λ n : nat . λ m...
Tá meio tarde pra dar uma resposta mas acho que o que acabou acontecendo é diferentes contribuidores foram traduzindo de locais diferentes e virou a bagunça que virou. No entanto...
O port pra C# será muito bem vindo. Testes unitários parece uma feature bacana, mas talvez seja overkill. Testes é feito pra garantir corretude computacional. Design patterns não têm valor...
@patrickmichalina, there is no other options that runs in virtual memory. We are trying to avoid having to setup xvfb in our CI machine just for running our tests. We...
#96 should fix this, but apparently this project is abandoned and I'm having trouble recompiling the .dll to provide. If someone can compile it would be awesome.
I would be very interested in this too. In fact I would expect that `Typing.Env.normalize_path_prefix` would achieve this, what are these `Env.normalize` functions actually doing?
I just bumped my PG from a 2 year old config and was driving myself nuts to find why the error wasn't working properly (hence got myself here). Thanks for...