blob: ce7cab1cbaf05e2652021db7a32045dc7ffc0049 (
plain)
1
2
3
4
5
6
7
|
(* Check let-ins in fix and Fixpoint *)
Definition foo := fix f (m : nat) (o := true) (n : nat) {struct n} :=
match n with 0 => 0 | S n' => f 0 n' end.
Fixpoint f (m : nat) (o := true) (n : nat) {struct n} :=
match n with 0 => 0 | S n' => f 0 n' end.
|
