blob: b5f0e730e3e23c9079d7544f6ff1c4e43992b4a8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* This has been a bug reported by Y. Bertot *)
Inductive expr : Set :=
b: expr -> expr -> expr
| u: expr -> expr
| a: expr
| var: nat -> expr .
Fixpoint f [t : expr] : expr :=
Cases t of
| (b t1 t2) => (b (f t1) (f t2))
| a => a
| x => (b t a)
end.
Fixpoint f2 [t : expr] : expr :=
Cases t of
| (b t1 t2) => (b (f2 t1) (f2 t2))
| a => a
| x => (b x a)
end.
|
