Module Core.GhostSource

Define a ghost signature that contain symbols used by the kernel but not defined by the user.

Sourceval sign : Sign.t

The signature holding ghost symbols.

The path of the ghost signature

Sourceval mem : Term.sym -> bool

mem s returns true if s is a ghost symbol.

Sourceval iter : (Term.sym -> unit) -> unit

iter f iters function f on ghost symbols.