package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type

This module is about the computation of an approximation of the head symbol of defined constants and local definitions; it provides the function to compute the head symbols and a table to store the heads

is_rigid tells if some term is known to ultimately reduce to a term with a rigid head symbol

val is_rigid : Environ.env -> Constr.constr -> bool
OCaml

Innovation. Community. Security.