def
definition
def or abbrev
name
show as:
view Lean formalization →
formal statement (Lean)
103def name : BookerPlotFamily → String
104 | overcomingTheMonster => "Overcoming the Monster"
105 | ragsToRiches => "Rags to Riches"
106 | theQuest => "The Quest"
107 | voyageAndReturn => "Voyage and Return"
108 | comedy => "Comedy"
109 | tragedy => "Tragedy"
110 | rebirth => "Rebirth"
111
112/-- The seven-element list of plot families. -/