MLML

This post supplements the post here.

I thought it might be a useful exercise to describe some of what goes into the tools described in that earlier post.

Mainly, I want to describe how the "markup language" MLML is implemented.

Tokenizer

inductive Token | ident (s : String) | strLit (s : String) | natLit (n : Nat) | boolLit (b : Bool) | lbrace | rbrace | lbracket | rbracket | comma | colon | equals | eof | comment (s : String) deriving Repr, BEq

The function tokenize then has signature def tokenize (input : String) : List Token.