Skip to content
Juvix imports 

module arch.system.types.resource_logic_proof;

import prelude open;

Resource logic proofs

A resource logic proof is a term of type ResourceLogicProof. Resource logic proofs attest to validity of resource_logics.

ResourceLogicProof

type ResourceLogicProof := mkResourceLogicProof@{};
Arguments
instance
the instance of the resource logic proof
witness
the witness of the resource logic proof
constraints
the constraints of the resource logic proof

Purpose

Todo

Explain the purpose of resource logic proofs.

Properties

Todo

Explain the properties of resource logic proofs.