MPRI PRFA 2025 Test file

Go back to the course page.

This test file should run perfectly if you have Rocq 9.0 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.
Cannot find a physical path bound to logical path All with prefix MetaRocq.Template.

(* Testing Equations *)
Equations eq_test (x : bool) : nat :=
  eq_test true := 12 ;
  eq_test false := 1.

(* Testing MetaRocq *)
MetaRocq Quote Definition eq_test_term := eq_test.
Print eq_test_term.