5.1. Literal Pattern

A literal pattern matches only the same literal value. It is often used in clausal definitions of functions.

5.1.1. Syntax

[37]LiteralPattern::= Literal  

5.1.2. Type

When a literal pattern is matched against a type T , the type of the literal value must be a subtype of the type T . The match produces an empty typing context, since it binds no variables.

5.1.3. Examples

Implication by Cases
{- Defining logical implication by cases -}

def implies(true, true) = true
def implies(true, false) = false
def implies(false, true) = true
def implies(false, false) = true

implies(false, false)


5.1.4. Related Links

Related Tutorial Sections