Module declaration 

Structs

AdtDecl

Axiom

Condition

A term with an “expl:” label (includes the “expl:” prefix)

Constant

ConstructorDecl

Contract

FieldDecl

Goal

LogicDecl

LogicDefn

Meta

MetaIdent

Module

Predicate

Signature

Span

Use

Enums

Attribute

Decl

DeclKind

MetaArg

Example: in meta "rewrite_def" function f, function is a Keyword and f is an Ident

SumRecord

TyDecl

ValKind