Documentation

Lean.Compiler.LCNF.ScopeM

@[reducible, inline]

A general abstraction for the idea of a scope in the compiler.

Clear the current scope for the monadic action x, afterwards continuing with the old one.

Check whether fvarId is in the current scope, that is, was declared within the current fun declaration that is being processed.

Add a new FVarId to the current scope.

Equations