GV68 assurance

GV68 is statically satisfied by typed governance identifiers and the readable pending/completed roadmap item constructors used by the DSL.

{-# OPTIONS --safe #-}

module Govenv.Assurance.GV68 where

open import Govenv.Kernel.Assurance using (StaticEvidence; staticEvidence)
open import Govenv.Kernel.Identifier using (GovernanceId; GV)
open import Govenv.Kernel.Roadmap using (Forest; GovernanceSpec; _◇; _✓)

record Proposition : Set where
  constructor satisfied
  field
    typedGovernanceId : GovernanceId 68 "assurance-governance"
    pendingNotation : Forest GovernanceSpec
    completedNotation : Forest GovernanceSpec

proof : Proposition
proof = satisfied
  (GV 68 "assurance-governance")
  (GV 68 "assurance-governance" ◇)
  (GV 68 "assurance-governance" ✓)

evidence : StaticEvidence 68
evidence = staticEvidence Proposition proof