module module

`IndisputableMonolith.Gravity.ConditionalSlot`

show as: view Lean formalization →

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

generate prose now

declarations in this module (15)

structure W L13
structure ConditionalSlot L28
structure VacuousWitnessShell L63
theorem vacuousWitnessShell_always_inhabited L71
theorem vacuousWitnessShell_inhabited_regardless L77
theorem conditionalSlot_nonempty_iff L91
theorem conditionalSlot_true_inhabited L99
theorem conditionalSlot_false_not_inhabited L106
structure TwoAssumptionShell L120
theorem twoAssumptionShell_always_inhabited L128
structure LiftedTwoAssumption L132
theorem liftedTwoAssumption_nonempty_iff L138
structure PatternALiftStatus L147
def patternALiftStatus L157
theorem pattern_a_one_statement L165