Module universe 

Structs

Universe 🔒

A “universe” defines the set of all terms (types/permissions/etc) in a program. The root universe Universe::ROOT consists of the terms the user wrote. We create other universes synthetically to create free universal variables. For example, in a closure body, we are in a distinct universe, which allows us to define closures that can reference a (generic) type T that doesn’t exist in the parent universe.