Code

Add probabilistic reasoning#48

Code

Merged

HarrisonGrodin merged 18 commits intomainjonsterling/agda-calf:mainfrom probability/basicsjonsterling/agda-calf:probability/basicsCopy head branch name to clipboardOct 9, 2023

+504-20

Commits

Commits on Mar 29, 2023

• Update to standard-library-2.0

  Show description for 1721233
  HarrisonGrodin

  committed
  1721233

  Copy full SHA for 1721233

• Implement basics of rational unit interval

  HarrisonGrodin

  committed
  b07de67

  Copy full SHA for b07de67

Commits on Apr 10, 2023

• Reorganize Interval around ∧ and ∨

  HarrisonGrodin

  committed
  ce78081

  Copy full SHA for ce78081

• Define flip primitive

  HarrisonGrodin

  committed
  36ad730

  Copy full SHA for 36ad730

• Update Calf to agda-stdlib 2.0

  HarrisonGrodin

  committed
  be5729f

  Copy full SHA for be5729f

• Add flip/step law

  HarrisonGrodin

  committed
  698f196

  Copy full SHA for 698f196

• Remove cancellativity from cost monoids

  HarrisonGrodin

  committed
  f9127b0

  Copy full SHA for f9127b0

• Add ℚ-CostMonoid

  HarrisonGrodin

  committed
  fb923bd

  Copy full SHA for fb923bd

• Merge branch 'main' into probability/basics

  HarrisonGrodin

  committed
  fe66a56

  Copy full SHA for fe66a56

Commits on Apr 11, 2023

• Write sample randomized algorithms

  HarrisonGrodin

  committed
  e5c0d24

  Copy full SHA for e5c0d24

Commits on May 26, 2023

• Merge branch 'main' into probability/basics

  HarrisonGrodin

  committed
  2c4dc3e

  Copy full SHA for 2c4dc3e

Commits on Jul 2, 2023

• Merge branch 'main' into probability/basics

  HarrisonGrodin

  committed
  3eacd67

  Copy full SHA for 3eacd67

Commits on Oct 9, 2023

• Merge branch 'decalf' into probability/basics

  HarrisonGrodin

  committed
  4e59488

  Copy full SHA for 4e59488

• Move flip to Decalf

  HarrisonGrodin

  committed
  dc4c78c

  Copy full SHA for dc4c78c

• Add sublist example

  HarrisonGrodin

  committed
  340e239

  Copy full SHA for 340e239

• Add probabilistic bound for map

  HarrisonGrodin

  committed
  c92236a

  Copy full SHA for c92236a

• Delete Randomized

  Show description for 291f09e
  HarrisonGrodin

  committed
  291f09e

  Copy full SHA for 291f09e

• Fix PredExp2

  HarrisonGrodin

  committed
  282e6d6

  Copy full SHA for 282e6d6