Parsing floats for a DSL

Stream: metaprogramming / tactics

[Danaël Carbonneau]

For a small project, i want to emebed a small DSL with probabilistic constructs (in order to be able to extract an AST), I followed a small tutorial (using the elaborator), but i'm stuck on how to deal with floats (i really need them since i'm working with probabilistic constructs...), it's not mentionned in the file that defines numeric literals (Parser/Extra.lean). Is there an easy way to parse floats ?

[Damiano Testa]

Does docs#Lean.Parser.scientificLit help?

[Danaël Carbonneau]

I think that it might be my last resort...