Documentation

Cedar.Thm.Data.LT

This file contains proofs that the less-than (<) relation on Cedar values is strict.

source
instance Cedar.Thm.IPNetPrefix.strictLT {w : Nat} :
Data.StrictLT (Spec.Ext.IPAddr.IPNetPrefix w)
source
instance Cedar.Thm.CIDR.strictLT {w : Nat} :
Data.StrictLT (Spec.Ext.IPAddr.CIDR w)
source
instance Cedar.Thm.IPNet.strictLT :
Data.StrictLT Spec.Ext.IPAddr.IPNet
source
instance Cedar.Thm.Datetime.strictLT :
Data.StrictLT Spec.Ext.Datetime
source
instance Cedar.Thm.Duration.strictLT :
Data.StrictLT Spec.Ext.Datetime.Duration
source
instance Cedar.Thm.Ext.strictLT :
Data.StrictLT Spec.Ext
source
instance Cedar.Thm.Name.strictLT :
Data.StrictLT Spec.Name
source
instance Cedar.Thm.EntityUID.strictLT :
Data.StrictLT Spec.EntityUID
source
instance Cedar.Thm.Prim.strictLT :
Data.StrictLT Spec.Prim
source
instance Cedar.Thm.Value.strictLT :
Data.StrictLT Spec.Value