Bosatsu/Nothing

Index

• Types: Nothing
• Values: impossible

Types

Nothing

In a total language, it is not possible to create a value with the type of magic

type Nothing

Values

impossible

since, we cannot create an instance of Nothing assuming we have one is a contradiction, so anything is possible

def impossible[a](n: Nothing) -> a