Alessio Coltellacci
Alessio Coltellacci
I am not sure that the PR works correctly. For example, if you change this Lemma in tests/OK/rewrite2.lp, it is impossible to unfold the definition of neither `p` or `q`....
The merge of #12 is still blocking because of [issue #4055](https://github.com/apache/pulsar/issues/4055). Until they have fix this issue we'll not be able to build the project with the pulsar-go-client library. :confused:
The official pulsar client is still in WIP and based on C++ which make difficult to use it. We decided to use a non-official client: [github.com/apache/pulsar-client-go](https://github.com/apache/pulsar-client-go).
Hello @JulienBe , I apologize for the delay of my response. I was a little busy last week by another project. In regards to this issue, I removed temporarily the...
how and where we should save the current bbolt DB ?
We have to convert the video in a GIF format (I'll do it). The github README doesn't support video for now.
cc [@ltearno](https://github.com/ltearno)
I played with the `eval` tactic with the definitions in [Tactic.lp](https://github.com/fblanqui/lambdapi/blob/master/tests/OK/Tactic.lp). This proof script cannot be unified. ``` symbol simp1 (x: τ nat) : π (x + 0 = x);...
Do we have a way to use the eval tactic on a proof that generates subgoals? For example, if we want to prove `π (((⊤ = ⊤) ∨ (⊤ =...
Yeah, np we can switch to the Discussion tab.