| 20 | /// single representation for mutual block processing. |
| 21 | #[derive(Clone, PartialEq, Eq, Debug)] |
| 22 | pub struct Def { |
| 23 | /// Fully-qualified name of the definition. |
| 24 | pub name: Name, |
| 25 | /// Universe-polymorphic level parameter names. |
| 26 | pub level_params: Vec<Name>, |
| 27 | /// The type of the definition. |
| 28 | pub typ: Expr, |
| 29 | /// The kind of definition (definition, theorem, or opaque). |
| 30 | pub kind: DefKind, |
| 31 | /// The definition body. |
| 32 | pub value: Expr, |
| 33 | /// Reducibility hints for the kernel. |
| 34 | pub hints: ReducibilityHints, |
| 35 | /// Safety classification. |
| 36 | pub safety: DefinitionSafety, |
| 37 | /// Names of all constants in the same mutual block. |
| 38 | pub all: Vec<Name>, |
| 39 | } |
| 40 | |
| 41 | impl Def { |
| 42 | /// Constructs a `Def` from a [`DefinitionVal`]. |
no outgoing calls
no test coverage detected