blob: 29c920f073fb719e188e91fadfa7ec4336831285 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
From Coq Require Import Arith.
Require Import Equations.Prop.Equations.
Set Implicit Arguments.
Set Primitive Projections.
Unset Printing All.
Scheme tree_forest_rec := Induction for tree Sort Set
with forest_tree_rec := Induction for forest Sort Set.
Fail Definition x : unit := 3.
admit.
Equations? neg (b : bool) : bool :=
neg true := false;
neg false := true.
|
