sorear / smetamath-rs

sorear's Metamath system engine - version 3 Rust
Apache License 2.0
22 stars 6 forks source link

Add $j parsing #31

Open digama0 opened 8 years ago

digama0 commented 8 years ago

A parsing algorithm for $j comments is needed to get basic grammar data, in particular, the identification of syntax proofs by typecode.