Test file for 2026

This test file should run perfectly if you have Rocq 9.2 installed as well as the required Equations and MetaCoq version.

You only need to make sure you can interpret the whole file, not understand it.

(* This should test that you have Rocq installed *)
From Stdlib Require Import Lia.

(* This should test that you also have Equations *)
From Equations Require Import Equations.

(* And MetaRocq Template *)
From MetaRocq.Template Require Import All.

(* Testing Equations *)
Equations eq_test (x : bool) : nat :=
  eq_test true := 12 ;
  eq_test false := 1.
eq_test_equation_1 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_equation_2 has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_graph_correct has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining
eq_test_elim has type-checked, generating 1 obligation
Solving obligations automatically...
No more obligations remaining

(* Testing MetaRocq *)
MetaRocq Quote Definition eq_test_term := eq_test.
Print eq_test_term.
eq_test_term =
tConst (MPfile ["test_file"%bs]%list, "eq_test"%bs) []%list
     : term

Scheme All for list.