Library Mtac2Tests.kind_of_term

Require Import Mtac2.Base.
Import M.

Definition test := ltac:(mrun (isLambda (fun x:nat=>x))).

Goal eval (isLambda (fun x:nat=>x)) = true. reflexivity. Qed.

Goal eval (isProd (forall x:nat, True)) = true. reflexivity. Qed.

Goal eval (isCast (True : Prop)) = true. reflexivity. Qed.

Goal eval (isApp (id 0)) = true. reflexivity. Qed.

Goal eval (isConst (@id)) = true. reflexivity. Qed.

Goal eval (isConstruct S) = true. reflexivity. Qed.