Quelle  ltac2_notations_eval_in.out   Sprache: unbekannt

- : constr =
constr:((fix add (n m : nat) {struct n} : nat :=
           match n with
           | 0 => m
           | S p => S (add p m)
           end)
          (1 + 2) 3)
- : constr = constr:(S (0 + 2 + 3))
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(6)
- : constr = constr:(1 + 2 + 3)
- : constr = constr:(1 + 2 + 3)
- : constr list =
[constr:(0 <> 0); constr:(0 = 0 -> False);
 constr:((fun P : Prop => P -> False) (0 = 0)); constr:(0 <> 0)]