Browse Source

Add definition of negligible.

idris
Thomas Kerber 1 year ago
parent
commit
502f9059ce
Signed by: Thomas Kerber <t.kerber@ed.ac.uk> GPG Key ID: 8489B911F9ED617B
1 changed files with 3 additions and 0 deletions
  1. +3
    -0
      Yggdrasil/Distribution.idr

+ 3
- 0
Yggdrasil/Distribution.idr View File

@@ -113,3 +113,6 @@ infixr 5 $=

data ($=) : D a -> D a -> Type where
EEq : Eq a => ((x : a) -> DualEvent {d1=d1} {d2=d2} f p e1 e2) -> d1 $= d2

negligible : Nat -> QQ
negligible n = Pos (replicate n L)

Loading…
Cancel
Save