DeepSpec/InteractionTrees

Issues

• Error installing coq-itree 5.1.1 with coq 8.18.0

  #259 opened 8 months ago by RalfJung
  3

• Consolidate stateT to extlib?

  #258 opened a year ago by elefthei
  4

• Universe inconsistency when paired with RelationAlgebra

  #254 opened a year ago by YaZko
  6

• `observe` vs `_observe`

  #251 opened a year ago by wkolowski
  0

• interp_prop is in the wrong place

  #243 opened 2 years ago by Zdancewic
  1

• Make `IForest`'s bind associative

  #240 opened 2 years ago by Lysxia
  0

• Compatibility fixes

  #199 opened 3 years ago by Lysxia
  0

• Reduce use of classical axioms

  #233 opened 2 years ago by Lysxia
  0

• Consider adding Hint Mode for typeclasses

  #230 opened 2 years ago by palmskog
  0

• Don't use `core` hint database?

  #222 opened 3 years ago by Lysxia
  1

• Throw exception in rec-fix

  #149 opened 3 years ago by liyishuai
  1

• Replace uses of strong excluded middle with choice

  #219 opened 3 years ago by Lysxia
  0

• Relating interaction tree and small-step semantics

  #176 opened 3 years ago by alxest
  5

• Encoding impure higher-order function with ktree

  #179 opened 3 years ago by alxest
  3

• Use `#[export]` instead of `#[global]`?

  #221 opened 3 years ago by Lysxia
  0

• Universe inconsistency

  #172 opened 4 years ago by alxest
  4

• Open Scope -> Local Open Scope

  #203 opened 3 years ago by Lysxia
  0

• re-defining monad notations

  #156 opened 3 years ago by vzaliva
  3

• Build documentation using dune instead of make

  #201 opened 3 years ago by Lysxia
  0

• Question: importing twice breaks notation

  #198 opened 3 years ago by alxest
  3

• Github pages

  #122 opened 3 years ago by Lysxia
  1

• Check axioms in CI

  #195 opened 3 years ago by Lysxia
  0

• Unwanted universe constraints?

  #193 opened 3 years ago by alxest
  1

• Prove (or disprove) "iter after iter" equation

  #187 opened 4 years ago by Lysxia
  1

• Move `MonadTheory` into ext-lib

  #140 opened 5 years ago by Lysxia
  4

• CI with Coq master

  #155 opened 4 years ago by Lysxia
  2

• Put notations in modules

  #160 opened 4 years ago by Lysxia
  1

• MonadLaws duplicated

  #177 opened 4 years ago by vzaliva
  4

• ITree.iter is not executable

  #182 opened 4 years ago by namefanwjcom
  1

• Question: Is this `Tau` essential?

  #178 opened 4 years ago by alxest
  3

• Bind notation with type annotation

  #174 opened 4 years ago by alxest
  3

• Unexpected definition of `mrec_fix`

  #170 opened 4 years ago by Mbodin
  3

• Improve mrec-fix notation

  #173 opened 4 years ago by Lysxia
  0

• Find/Make a Category Theory Library

  #167 opened 4 years ago by Lysxia
  3

• Can and should KTrees be generalized?

  #102 opened 4 years ago by YaZko
  11

• Publishing ITree library for Coq 8.11 on OPAM?

  #164 opened 4 years ago by lastland
  1

• Ignoring some event?

  #163 opened 4 years ago by alxest
  4

• Rewriting is slow

  #161 opened 4 years ago by Lysxia
  0

• Remove confusing notations

  #154 opened 4 years ago by Lysxia
  1

• Don't use ExtLib 0.10.2

  #150 opened 4 years ago by liyishuai
  0

• Compile issue with Basics.v

  #146 opened 5 years ago by tpottei1
  4

• Shortcomings of subevents

  #130 opened 5 years ago by YaZko
  5

• How to define morphism equivalence

  #115 opened 5 years ago by Lysxia
  3

• Reasoning Principles for ITrees

  #123 opened 5 years ago by gilhur
  2

• Rewriting with `interp_bind` doesn't properly generalize

  #125 opened 5 years ago by jeehoonkang
  4

• Terminology and naming?

  #118 opened 5 years ago by Zdancewic
  1

• Generalized rewriting for applied morphisms

  #101 opened 5 years ago by Lysxia
  5

• Document the compiler example

  #91 opened 5 years ago by Zdancewic
  0

• Split compiler example into its own subdirectory

  #90 opened 5 years ago by Zdancewic
  2

• Duplicate names

  #112 opened 5 years ago by Lysxia
  5