From Coq Require Import Arith.
Require Import Equations.Prop.Equations.
Set Implicit Arguments.
Set Primitive Projections.
Set Warnings "-extraction".
Set Typeclasses Depth 14.
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.
String Notation foo bar baz [ via nat mapping [ S => s, [O] => o ], abstract after 10 ]
  : w_scope.
Elpi Program b lp:{{ }}.
Elpi test.
