Quelle  ltac2_match.v   Sprache: unbekannt

Require Import Ltac2.Ltac2.

Ltac2 Type rec autre :=
[  C | D | E (autre) | F (autre, autre) | H (autre) | I | J | K (string) ].

Ltac2 rec autre x := match x with
| C,_,_ => 1
| _,C,_ => 2
| D,D,_ => 3
| (D|(F _ _)|(H _)|K _),_,_ => 4
| (_, (D|I|E _|F _ _|H _|K _), _) => 8
| (J,J,((C|D) as x |E x|F _ x)) | (J,_,((C|J) as x)) => autre (x,x,x)
| (J, J, (I|H _|K _)) => 9
| I,_,_ => 6
| E _,_,_ => 7
end.



Ltac2 Type t_l := [A | B].

Ltac2 f x := match x with
  |  _, _, _, _, _, _, _, _, _, _, _, _, _, B, _, _ => "0"
  |  _, _, _, B, A, _, _, _, _, _, _, _, _, _, _, _ => "1"
  |  _, _, _, B, _, A, _, _, A, _, _, _, _, _, _, _ => "2"
  |  _, _, _, _, _, _, _, _, _, _, B, A, _, A, _, _ => "3"
  |  _, _, _, _, _, _, _, B, _, _, _, _, B, _, A, A => "4"
  |  A, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _ => "5"
  |  _, _, _, _, _, _, _, B, _, B, _, _, _, _, _, _ => "6"
  |  _, B, _, _, _, _, _, _, _, _, _, _, _, _, _, _ => "7"
  |  _, A, A, _, A, _, B, _, _, _, _, _, _, _, _, B => "8"
  |  _, _, _, _, B, _, _, _, _, _, _, _, _, _, B, _ => "9"
  |  _, _, _, _, _, _, _, _, _, _, _, B, _, _, _, _ => "10"
  |  _, _, _, _, _, A, _, _, _, _, B, _, _, _, _, _ => "11"
  |  B, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _ => "12"
  |  _, _, _, _, _, _, _, _, _, _, _, _, _, _, _, _ => "13"
end.

Ltac2 Eval f (B, A, A, A, A, A, A, A, A, A, A, B, A, A, A, A).
Ltac2 Eval f (B, A, A, A, A, A, A, A, A, A, A, A, A, A, A, A).