Yeah, it works fine on demo0.mm. I did some examples by hand to make sure 
that disjointment constraints are verified properly as well.

Dana utorak, 3. prosinca 2019. u 16:18:22 UTC+1, korisnik Antony Bartlett 
napisao je:
>
> Uncompressing the entire set.mm database was last discussed here
>
> https://groups.google.com/forum/#!msg/metamath/Hey2L9f1ULk/vXMWVcI5DwAJ
>
> Can your verifier check demo0.mm yet? (
> https://github.com/david-a-wheeler/metamath-test/blob/master/demo0.mm)
>
>     Best regards,
>
>         Antony
>
>
> On Tue, Dec 3, 2019 at 2:32 PM Marko Grdinic <mra...@gmail.com 
> <javascript:>> 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 meta...@googlegroups.com <javascript:>.
>> To view this discussion on the web visit 
>> https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com
>>  
>> <https://groups.google.com/d/msgid/metamath/fbd4651b-9429-4ecb-96ae-db8ebbaa7431%40googlegroups.com?utm_medium=email&utm_source=footer>
>> .
>>
>

-- 
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/a299c546-ecc3-4020-a199-139d2c00a2a7%40googlegroups.com.

Reply via email to