search

meta-logic / sml-to-coq

A tool that translates SML code to Coq
GNU General Public License v3.0
6 stars 0 forks source link

Use of patternFailure #11

Open gisellemnr opened 3 years ago

gisellemnr commented 3 years ago

Could we replace the use of patternFailure axioms on value declarations:

Definition x := match [1; 2; 3] with (x :: l) => x
                                   | _ => patternFailure
                end .
Definition l := match [1; 2; 3] with (x :: l) => l
                                   | _ => patternFailure
                end .

by

Definition x := match [1;2;3] as l return l <> [] -> nat with 
  | x :: _ => fun _ => x 
  | _ => fun H => match H eq_refl with end end.

Definition l := match [1;2;3] as l1 return l1 <> [] -> list nat with 
  | _ :: l => fun _ => l 
  | _ => fun H => match H eq_refl with end end.

Compute x.
Compute l.

??

Notice that x and l have different types in the first and second examples.