[Practico 5] Ej 5 Error Pattern "_" is redundant in this clause.

[Practico 5] Ej 5 Error Pattern "_" is redundant in this clause.

de Agustin Di Vincezo Fernandez -
Número de respuestas: 2

Buenas,

Estoy con el ejercicio 5.2 del practico 5, pero esta consulta es mas genérica sobre pattern matching. 

Al definir una funcion recursiva, utilizando _ como patron por defecto, obtengo el siguiente error:

Pattern "_" is redundant in this clause.

Concretamente mi definición intenta ser esta:

Fixpoint deleteAll (a:A)(l:List) {struct l}: List:=
  match l with
   |nullL  => nullL
   |consL x s =>  match x with
          | a => deleteAll a s
          | _ => consL x (deleteAll a s)
           end 
  end.

Cual es la forma correcta de definir un patron para x cuando es diferente de a?

Desde ya gracias

Saludos

En respuesta a Agustin Di Vincezo Fernandez

Re: [Practico 5] Ej 5 Error Pattern "_" is redundant in this clause.

de Carlos Luna -
Hola.

Al poner una variable (a) como patrón, cualquier constructor de un tipo de datos unifica con ella. Luego, los casos restantes son redundantes/innecesarios en ese pattern matching: _ => consL x (deleteAll a s).

Por otra parte, no estas analizando bien la igualdad de x y a. Los patterns son para los constructores de los tipos de datos. Debería ser esa parte algo como:

match (equal x a) with
          | true => deleteAll a s
          | _ => consL x (deleteAll a s)
           end 

Donde equal sería la (función de) igualdad booleana de elementos de tipo A. Para bool los contructores son true y false.

Saludos Carlos