From 24845ef25e12864711552ebc75a1f54903bee50c Mon Sep 17 00:00:00 2001 From: Greg Brown Date: Sat, 9 Apr 2022 16:49:49 +0100 Subject: A proof of the simplest form of Barrett reduction. --- Everything.agda | 3 +++ 1 file changed, 3 insertions(+) (limited to 'Everything.agda') diff --git a/Everything.agda b/Everything.agda index cd0f148..2f76af0 100644 --- a/Everything.agda +++ b/Everything.agda @@ -84,6 +84,9 @@ import Helium.Algebra.Structures -- Definition of types and operations used by the Armv8-M pseudocode. import Helium.Data.Pseudocode.Algebra +-- A proof of correctness for Barrett reduction. +import Helium.Data.Pseudocode.Algebra.Barrett + -- Algebraic properties of types used by the Armv8-M pseudocode. import Helium.Data.Pseudocode.Algebra.Properties -- cgit v1.2.3