BitML.Contracts

Source code on Github
open import Prelude.Init; open SetAsType
open import Prelude.DecEq

open import BitML.BasicTypes

module BitML.Contracts ⋯ where

open import BitML.Contracts.Types ⋯ public
module Induction where
  open import BitML.Contracts.Induction ⋯ public
open import BitML.Contracts.Collections ⋯ public
open import BitML.Contracts.Validity ⋯ public
open import BitML.Contracts.ModuleMacros ⋯ public
open import BitML.Contracts.Subterms ⋯ public