inductive definition def or abbrev

`Primitive`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  18inductive Primitive
  19  | Love | Justice | Forgiveness | Wisdom | Courage | Temperance | Prudence
  20  | Compassion | Gratitude | Patience | Humility | Hope | Creativity | Sacrifice
  21  deriving DecidableEq, Repr
  22
  23/-- Canonical primitive order as a list. -/

used by (22)

From the project-wide theorem graph. These declarations reference this one in their body.

Centering in IndisputableMonolith.Chemistry.CrystalSymmetry decl_use
aggCoeff in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_append in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_flatMap in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_rowMoves in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_rowMoves_aux in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_rowMoves_aux_axiom in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_rowMoves_aux_theorem in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
aggCoeff_rowMoves_of_ne in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
mem_toMoves_of_coeff_ne_zero in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
MicroMove in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
NormalForm in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
pair_mem_toMoves_map in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
primitive_mem_order in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
primitiveOrderList in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
rowMoves_mem_of_coeff_ne_zero in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
sumCoeffs_toMoves in IndisputableMonolith.Ethics.Virtues.NormalForm decl_use
physical_light_not_first in IndisputableMonolith.Foundation.PreTemporalForcingOrder decl_use
Recognizer in IndisputableMonolith.Foundation.RecognizerInducesLogic decl_use
unification in IndisputableMonolith.Foundation.RecognizerInducesLogic decl_use
deltaOf in IndisputableMonolith.Masses.SectorPrimitive decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use

depends on (2)

Lean names referenced from this declaration's body.

as in IndisputableMonolith.Foundation.SimplicialLedger.ContinuumBridge decl_use
Primitive in IndisputableMonolith.Masses.SectorPrimitive decl_use