SilverSight/coq/AVMIsa/test_avm.v at main - allaun/SilverSight - Forgejo: Beyond coding. We Forge.

allaun/SilverSight

mirror of https://github.com/allaunthefox/SilverSight.git synced 2026-07-31 01:25:21 +00:00

allaun 069e54d8e9 fix(coq): migrate all files to Rocq 9.0 imports (ZCompat, no ZArith)

All 5 Coq files now use:
  From Corelib Require Import BinNums PosDef NatDef IntDef.
  Require Import SilverSight.coq.ZCompat.

instead of Require Import ZArith Lia.

Build: 5 Coq files, 0 errors

2026-07-01 23:21:29 -05:00

17 lines

367 B

Coq

Raw Permalink Blame History

 (* AVM ISA v1 — Coq Test Harness (Rocq 9.0) *)
 From Corelib Require Import BinNums PosDef NatDef IntDef Init.Datatypes.
 Require Import SilverSight.coq.ZCompat.
 Require Import SilverSight.coq.AVMIsa.avm.
 Local Open Scope Z_scope.
 Definition QS := 65536.
 Example test_basic_add : True.
 Proof.
   exact I.
 Qed.
 Example test_saturation : True.
 Proof.
   exact I.
 Qed.