Tests for Modules

axiom GaudisCrypt.sig : ProcedureSignature

def GaudisCrypt.TestModule [ProgramSpec] : Type (max 1 u_1)

Equations

• GaudisCrypt.TestModule = GaudisCrypt.Module ((GaudisCrypt.ModuleTypeRep.proc GaudisCrypt.sig).prod (GaudisCrypt.ModuleTypeRep.proc GaudisCrypt.sig))

noncomputable def GaudisCrypt.TestModule.main [ProgramSpec] (m : TestModule) : Module (ModuleTypeRep.proc sig)

Equations

• m.main = GaudisCrypt.Module.fst' m

noncomputable def GaudisCrypt.TestModule.aux [ProgramSpec] (m : TestModule) : Module (ModuleTypeRep.proc sig)

Equations

• m.aux = GaudisCrypt.Module.snd' m

structure GaudisCrypt.TestModuleStruct [ProgramSpec] : Type (max 1 u_1)

• main : Module (ModuleTypeRep.proc sig)
• aux : Module (ModuleTypeRep.proc sig)

noncomputable def GaudisCrypt.TestModuleStruct.destruct [ProgramSpec] (str : TestModuleStruct) : TestModule

Equations

• str.destruct = str.main.pair' str.aux

noncomputable def GaudisCrypt.TestModule.mk [ProgramSpec] (str : TestModuleStruct) : TestModule

Equations

• GaudisCrypt.TestModule.mk str = str.main.pair' str.aux

axiom GaudisCrypt.testMain [ProgramSpec] : Module (ModuleTypeRep.proc sig)

axiom GaudisCrypt.testAux [ProgramSpec] : Module (ModuleTypeRep.proc sig)

noncomputable def GaudisCrypt.myMod [ProgramSpec] : TestModule

Equations

• GaudisCrypt.myMod = GaudisCrypt.TestModule.mk { main := GaudisCrypt.testMain, aux := GaudisCrypt.testAux }

theorem GaudisCrypt.test [ProgramSpec] : myMod.main = testMain