Simple Probability Execution

Stream: new members

[Yuanbo Li]

Hi everyone, I'm a student working using Lean4 to make some proves on L-System and procedural grammars. And I hope to know how to execute simply probabilities using lean.

For instance, a grammar can be A -> B (prob0.5) and A ->AB (prob0.5). Could anyone offer me some idea what package should I look into to write/execute these kind of grammars? Thank you!