Ecosyste.ms: Issues

An open API service for providing issue and pull request metadata for open source projects.

GitHub / alexkeizer/qpftypes issues and pull requests

#59 - chore: bump toolchain to v4.14.0

Pull Request - State: closed - Opened by alexkeizer about 2 months ago - 1 comment

#58 - feat: Expr-level shape type definition

Pull Request - State: closed - Opened by alexkeizer about 2 months ago

#57 - Update to 14.4?

Issue - State: closed - Opened by hgoldstein95 about 2 months ago - 2 comments

#56 - Implement ITrees manually

Pull Request - State: open - Opened by Kiiyya 2 months ago

#55 - refactor: remove `IsPolynomial` class

Pull Request - State: closed - Opened by alexkeizer 2 months ago

#54 - fix: remove `MvFunctor` instance arg from `IsPolynomial`

Pull Request - State: closed - Opened by alexkeizer 2 months ago

#53 - Remove `IsPolynomial`

Issue - State: closed - Opened by alexkeizer 2 months ago

#52 - Fix: Make `Prod'` universe-polymorphic

Pull Request - State: closed - Opened by Kiiyya 2 months ago - 1 comment

#51 - Instance `MvFunctor Prod'` is not universe-polymorphic

Issue - State: closed - Opened by Kiiyya 2 months ago - 2 comments

#50 - Make `qpf` macro support sigma types

Issue - State: open - Opened by Kiiyya 2 months ago

#49 - WIP: feat: define weak bisimulation for ITrees

Pull Request - State: open - Opened by alexkeizer 4 months ago

#48 - fix: update copyright info in License file

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#47 - feat: build ITree in CI

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#46 - feat: beginning of an ITree library

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#45 - feat: more descriptive tracing

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#44 - WIP: allow (co)datatypes without live variables

Pull Request - State: open - Opened by alexkeizer 4 months ago

#43 - feat: structure trace with trace nodes

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#42 - chore: bump toolchain to v4.12.0

Pull Request - State: closed - Opened by alexkeizer 4 months ago

#41 - feat: add DeepThunk

Pull Request - State: closed - Opened by Equilibris 6 months ago - 2 comments

#40 - feat: generalize constructor generation further

Pull Request - State: closed - Opened by Equilibris 6 months ago - 1 comment

#39 - refactor: prefer concat (++) over hand crafting names

Pull Request - State: closed - Opened by Equilibris 6 months ago - 1 comment

#38 - refactor: extract handling of RecForms

Pull Request - State: closed - Opened by Equilibris 6 months ago

#37 - feat: add the ability to access the uncurried base

Pull Request - State: closed - Opened by Equilibris 6 months ago

#36 - Codef 4 macro

Pull Request - State: open - Opened by Equilibris 6 months ago

#35 - Add the notion of a `DeepThunk` and generation for this

Pull Request - State: open - Opened by Equilibris 7 months ago - 1 comment

#34 - Generalize utility functions previously used for a single purpose

Pull Request - State: closed - Opened by Equilibris 7 months ago - 1 comment

#33 - chore: move Qpf constructor generation into separate file

Pull Request - State: closed - Opened by Equilibris 7 months ago - 3 comments

#32 - Chore: update to Lean v4.9.0

Issue - State: closed - Opened by alexkeizer 7 months ago

#30 - feat: add generation of inductive principles for basic ctors

Pull Request - State: closed - Opened by Equilibris 7 months ago

#29 - Feature: Syntax and delaborator for `TypeVec` and `Fin2`s

Issue - State: open - Opened by alexkeizer 7 months ago
Labels: easy

#29 - Feature: Syntax and delaborator for `TypeVec` and `Fin2`s

Issue - State: open - Opened by alexkeizer 7 months ago
Labels: easy

#27 - Revert "refactor: replace.lean"

Pull Request - State: closed - Opened by alexkeizer 8 months ago

#26 - Feature: basic pattern matching for data-types

Issue - State: open - Opened by alexkeizer 8 months ago

#25 - WIP: feat: allow limited type ascriptions in data/codata

Pull Request - State: open - Opened by alexkeizer 8 months ago - 3 comments

#24 - refactor: `is_trivial` check to be more succinct

Pull Request - State: closed - Opened by Equilibris 8 months ago

#23 - refactor: Replace struct

Pull Request - State: closed - Opened by Equilibris 8 months ago - 2 comments

#22 - refactor: update types in elabQpf to reflect the code

Pull Request - State: closed - Opened by Equilibris 8 months ago - 1 comment

#21 - refactor: factor elabQpf into separate functions

Pull Request - State: closed - Opened by Equilibris 8 months ago

#20 - Remove PFin2 in favour of Fin(2) using ulift

Issue - State: open - Opened by Equilibris 8 months ago

#19 - refactor: composition pipeline and qpf body parsing

Pull Request - State: closed - Opened by Equilibris 8 months ago - 2 comments

#18 - feat: support constructor arguments given as explicit binders

Pull Request - State: closed - Opened by Equilibris 8 months ago

#17 - Cleanup: make examples checked by CI

Issue - State: open - Opened by alexkeizer 8 months ago

#16 - Feature: Introduce explicit syntax to distinguish live and dead variables

Issue - State: open - Opened by alexkeizer 8 months ago
Labels: good first issue

#14 - chore: make tests less noisy

Pull Request - State: closed - Opened by alexkeizer 9 months ago

#13 - chore: remove `fin_destr` tactic

Pull Request - State: closed - Opened by alexkeizer 9 months ago

#12 - Cleanup: Consistent Code Formatting

Issue - State: open - Opened by alexkeizer 9 months ago

#11 - Feature: support constructor arguments given as binders

Issue - State: closed - Opened by alexkeizer 9 months ago
Labels: good first issue

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

Issue - State: open - Opened by alexkeizer 9 months ago - 1 comment

#9 - chore: upgrade to Lean v4.7.0

Pull Request - State: closed - Opened by alexkeizer 9 months ago

#8 - Cleanup: Get rid of `fin_destr` tactic in favour of Mathlib's `fin_cases`

Issue - State: closed - Opened by alexkeizer 9 months ago - 1 comment

#7 - feat: basic CI testing

Pull Request - State: closed - Opened by alexkeizer 12 months ago

#6 - fix: re-add `PFin2.elim0`

Pull Request - State: closed - Opened by monsterkrampe 12 months ago - 5 comments

#5 - feat: build up typeclass instances in the composition pipeline

Pull Request - State: closed - Opened by alexkeizer 12 months ago

#3 - Feature: Special-case types definable through just polynomial functors

Issue - State: open - Opened by alexkeizer 12 months ago
Labels: low prio

#2 - Timeout in typeclass synthesis of `∀ i, MvFunctor (_ i)`

Issue - State: closed - Opened by alexkeizer 12 months ago - 5 comments

#1 - feat: upgrade to Lean 4.5.0

Pull Request - State: closed - Opened by monsterkrampe 12 months ago - 3 comments