Re: [Metamath] Re: How to process dummylink?

[Mario Carneiro]

I agree; I think implementing compressed proof reading is worth the effort,
particularly because of the exponential speedup over uncompressed proofs
(in the worst case). The scheme is pretty simple to work with. Be sure to
read appendix C of the metamath book, which lays it all out clearly.

On Thu, Dec 5, 2019 at 12:10 PM Tony  wrote:

> I found proof decompression to be easier to implement than I thought it
> would be. The hardest part was just understanding how it works.
>
> On Tuesday, December 3, 2019 at 3:32:07 PM UTC+1, Marko Grdinic wrote:
>>
>> Well, at any rate as I've been working on this for 9 days now I'll stop
>> here. I do not feel like going those last few extra miles just to implement
>> proof decompression and test it thoroughly on the big library. I am not
>> sure how stringent the criteria for inclusion on that list of verifiers in
>> other languages are, but it might be good enough for consideration anyway
>> even in its current form.
>>
>> I am impatient to start studying set theory so I'll get to that. That was
>> what attracted me to Metamath in the first place. Doing this toy
>> implementation was a side quest.
>>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to metamath+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/c40d837c-6e17-4030-93c7-d72b35e817f5%40googlegroups.com
> 
> .
>

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAFXXJSsQyQfWNdj%3DJQSD-f6g_yV5YaiO1cEMiedpyfH5Fe2RwA%40mail.gmail.com.

[Metamath] Re: How to process dummylink?

[Tony]

I found proof decompression to be easier to implement than I thought it 
would be. The hardest part was just understanding how it works.

On Tuesday, December 3, 2019 at 3:32:07 PM UTC+1, Marko Grdinic wrote:
>
> Well, at any rate as I've been working on this for 9 days now I'll stop 
> here. I do not feel like going those last few extra miles just to implement 
> proof decompression and test it thoroughly on the big library. I am not 
> sure how stringent the criteria for inclusion on that list of verifiers in 
> other languages are, but it might be good enough for consideration anyway 
> even in its current form.
>
> I am impatient to start studying set theory so I'll get to that. That was 
> what attracted me to Metamath in the first place. Doing this toy 
> implementation was a side quest.
>

-- 
You received this message because you are subscribed to the Google Groups 
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/c40d837c-6e17-4030-93c7-d72b35e817f5%40googlegroups.com.