Documentation

GaudisCrypt.Language.ModulesTest

Tests for `Modules` #

axiom GaudisCrypt.sig :

ProcedureSignature

def GaudisCrypt.TestModule :

Equations

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

Instances For

noncomputable def GaudisCrypt.TestModule.main (m : TestModule) :

Module (ModuleTypeRep.proc sig)

Equations

m.main = GaudisCrypt.Module.fst' m

Instances For

noncomputable def GaudisCrypt.TestModule.aux (m : TestModule) :

Module (ModuleTypeRep.proc sig)

Equations

m.aux = GaudisCrypt.Module.snd' m

Instances For

structure GaudisCrypt.TestModuleStruct :

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

Instances For

noncomputable def GaudisCrypt.TestModuleStruct.destruct (str : TestModuleStruct) :

Equations

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

Instances For

noncomputable def GaudisCrypt.TestModule.mk (str : TestModuleStruct) :

Equations

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

Instances For

axiom GaudisCrypt.testMain :

Module (ModuleTypeRep.proc sig)

axiom GaudisCrypt.testAux :

Module (ModuleTypeRep.proc sig)

noncomputable def GaudisCrypt.myMod :

Equations

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

Instances For

theorem GaudisCrypt.test :

myMod.main = testMain