Lean 4 (Meta)programming Cookbook

Mutable Variables: Example🔗

Contributors: Siddhartha Gadgil

Mutable Variables: Example🔗

Mutable variables defined by IO.Ref and Std.Mutex cannot be evaluated in the same file where they are defined. Here, we continue the example of computing Catalan numbers from the previous recipe Mutable Variables across commands and show how to use mutable variables to preserve the computed values across different commands.

When we initially lookup the cached value of C(32), we get none since it has not been computed yet.

none#eval getCatalanCache? 32

After we compute C(32) using the catalanCached function, the value is stored in the cache. When we lookup the cached value of C(31), we get some 14544636039226909, which is the correct value of C(31).

55534064877048198#eval catalanCached 32 some 14544636039226909#eval getCatalanCache? 31 14544636039226909#eval catalanCached 31