CODEWITHSUNDEEP
functional-programmingisabelletheorem-proving
Yiyi
Yiyi

Reputation: 15

Ignore missing pattern in Isabelle

For example, I would like to define a function that extracts the first element of a list. For this function, I do not care about the case when the list is empty (e.g. I can make sure that every time I use the function, I will pass a non-empty list). But Isabelle would warn that

Missing patterns in function definition:
extracts [] = undefined

How can I deal with situations like this?

Upvotes: 1

Views: 115

Answers (1)

Javier Díaz
Javier Díaz

Reputation: 1081

You have quite a few options available, for example:

  1. fun extracts where "extracts xs = hd xs"
  2. definition extracts where [simp]: "extracts = hd"
  3. fun extracts where "extracts xs = (case xs of (x # _) ⇒ x)"
  4. fun extracts where "extracts (x # _) = x" | "extracts [] = undefined"

Upvotes: 2

Related Questions