alexkeizer/QpfTypes

Issues

• Update to 14.4?

  #57 opened 15 days ago by hgoldstein95
  0

• Remove `IsPolynomial`

  #53 opened 24 days ago by alexkeizer
  0

• Instance `MvFunctor Prod'` is not universe-polymorphic

  #51 opened 24 days ago by Kiiyya
  2

• Make `qpf` macro support sigma types

  #50 opened 25 days ago by Kiiyya
  0

• Enhancement: implement `Fix.cases` such that an entire recursion of the data structure is not required

  #31 opened 6 months ago by Equilibris
  0

• Chore: update to Lean v4.9.0

  #32 opened 3 months ago by alexkeizer
  0

• Feature: Syntax and delaborator for `TypeVec` and `Fin2`s

  #29 opened 6 months ago by alexkeizer
  0

• Indexed families should fast-fail rather than spin forever

  #28 opened 6 months ago by Equilibris
  0

• Feature: basic pattern matching for data-types

  #26 opened 6 months ago by alexkeizer
  0

• Remove PFin2 in favour of Fin(2) using ulift

  #20 opened 6 months ago by Equilibris
  0

• Feature: support constructor arguments given as binders

  #11 opened 6 months ago by alexkeizer
  0

• Feature: Accept some form of type ascriptions on `data` and `codata`

  #15 opened 7 months ago by alexkeizer
  0

• Cleanup: make examples checked by CI

  #17 opened 6 months ago by alexkeizer
  0

• Feature: Introduce explicit syntax to distinguish live and dead variables

  #16 opened 7 months ago by alexkeizer
  0

• Cleanup: get rid of noisy lines (e.g., `#check`)

  #10 opened 7 months ago by alexkeizer
  1

• Cleanup: Get rid of `fin_destr` tactic in favour of Mathlib's `fin_cases`

  #8 opened 7 months ago by alexkeizer
  1

• Cleanup: Consistent Code Formatting

  #12 opened 7 months ago by alexkeizer
  0

• Bug: Infinite loop when referring to a non-existent type

  #4 opened 10 months ago by alexkeizer
  0

• Feature: Special-case types definable through just polynomial functors

  #3 opened 10 months ago by alexkeizer
  0

• Timeout in typeclass synthesis of `∀ i, MvFunctor (_ i)`

  #2 opened 10 months ago by alexkeizer
  5