jvanbruegge/binder_datatypes

Issues

• Make tvsubst compose

  #12 opened a year ago by jvanbruegge
  0

• Make tvsubst allow mutual recursion

  #34 opened 6 months ago by jvanbruegge
  0

• Make sugar allow mutual recursion

  #37 opened 7 months ago by jvanbruegge
  0

• Make sugar allow passive positions

  #36 opened 7 months ago by jvanbruegge
  0

• Make tvsubst allow passive positions

  #35 opened 6 months ago by jvanbruegge
  0

• Register mixfix syntax associated with constructors

  #31 opened 8 months ago by jvanbruegge
  0

• Fix more_consumes vs nmajor cases bug

  #30 opened 8 months ago by jvanbruegge
  0

• Fix binder_induction in relators and under quantifiers

  #29 opened 8 months ago by jvanbruegge
  0

• Fix binder_induction method for mutual recursion and more than one variable kind

  #27 opened 8 months ago by jvanbruegge
  0

• Generalize vvsubst to allow mutual recursion and passive positions

  #16 opened 8 months ago by jvanbruegge
  0

• Allow to specify a predicate for the codomain of the recursor

  #23 opened 9 months ago by jvanbruegge
  0

• Allow to specify a predicate for the parameters in the recursor

  #15 opened 9 months ago by jvanbruegge
  0

• Investigate monomorphic recursor

  #22 opened 9 months ago by jvanbruegge
  0

• Allow to specify the minimum cardinal in the recursor again

  #18 opened 10 months ago by jvanbruegge
  0

• Generalize the recursor to allow passive positions and mutually recursive types

  #10 opened a year ago by jvanbruegge
  0

• Automate singular/list substitution

  #19 opened a year ago by jvanbruegge
  0

• Provide FFVars_tvsubst again

  #17 opened a year ago by jvanbruegge
  0

• Implement the corecursor

  #11 opened a year ago by jvanbruegge
  0

• Create a parser for the custom binder_datatype syntax

  #7 opened a year ago by jvanbruegge
  2

• Allow changing the names of the involved constants

  #9 opened a year ago by jvanbruegge
  0

• Create a binder_(co)primrec to define primitive recursive functions on binder_datatypes

  #8 opened a year ago by jvanbruegge
  0

• Do not generate a new class at every step of the composition or mrbnf definition

  #6 opened a year ago by jvanbruegge
  0