Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
Instances For
Equations
- Auto.MessageData.intercalate.go acc m (a :: as) = Auto.MessageData.intercalate.go (acc.compose (m.compose a)) m as
- Auto.MessageData.intercalate.go acc m [] = acc
Instances For
Equations
- Auto.MessageData.list as f = (Lean.toMessageData "[").compose ((Auto.MessageData.intercalate (Lean.toMessageData ", ") (List.map f as)).compose (Lean.toMessageData "]"))
Instances For
Equations
- Auto.MessageData.array as f = Auto.MessageData.list as.toList f