Search results

Fix arbitrary variables in the context for binder_induction

area: binder_induction

Priority: Low

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#95 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Jul 10, 2025

binder_induction avoiding an immediate argument of the inductive predicate fails

area: binder_induction

bugSomething isn't workingSomething isn't working

Status: Open.

#94 In jvanbruegge/binder_datatypes;

· dtraytel opened on Jul 8, 2025

Do not split user defined "raw" avoiding sets in binder_induction

area: binder_induction

bugSomething isn't workingSomething isn't working

Status: Open.

#91 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Jul 2, 2025

Dead variables example failing

area: mrbnf composition

bugSomething isn't workingSomething isn't working

Status: Open.

#90 In jvanbruegge/binder_datatypes;

· dtraytel opened on Jun 30, 2025

Allow to freely reorder parameters of binder_datatype

area: mrbnf fixpoint

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#80 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Apr 17, 2025

Replace BNFs with MRBNFs in Isabelle

Priority: Low

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#78 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Apr 16, 2025

Adapt recursor for multiple bounds for single free position

area: recursor

new featureAllows to define types that are currently impossible to defineAllows to define types that are currently impossible to define

Priority: Low

Status: Open.

#58 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Nov 7, 2024

Make binder_inductive automation work in more (all?) cases

area: binder_inductive

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#57 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Nov 5, 2024

Make sugar allow mutual recursion

area: sugar

new featureAllows to define types that are currently impossible to defineAllows to define types that are currently impossible to define

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#37 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Feb 26, 2024

Automate singular/list substitution

area: sugar

good first issueGood for newcomersGood for newcomers

new featureAllows to define types that are currently impossible to defineAllows to define types that are currently impossible to define

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#19 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Oct 17, 2023

Make tvsubst compose

new featureAllows to define types that are currently impossible to defineAllows to define types that are currently impossible to define

usabilityChanges that will make it nicer for the end userChanges that will make it nicer for the end user

Status: Open.

#12 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Aug 29, 2023

Implement the corecursor

new featureAllows to define types that are currently impossible to defineAllows to define types that are currently impossible to define

Status: Open.

#11 In jvanbruegge/binder_datatypes;

· jvanbruegge opened on Aug 29, 2023