Search results

Make <code>qpf</code> macro support sigma types

Status: Open.

#50 In alexkeizer/QpfTypes;

· Kiiyya opened on Dec 2, 2024

Enhancement: implement <code>Fix.cases</code> such that an entire recursion of the data structure is not required

low prio

Status: Open.

#31 In alexkeizer/QpfTypes;

· Equilibris opened on Jul 11, 2024

Feature: Syntax and delaborator for <code>TypeVec</code> and <code>Fin2</code>s

easy

Status: Open.

#29 In alexkeizer/QpfTypes;

· alexkeizer opened on Jul 6, 2024

Indexed families should fast-fail rather than spin forever

Status: Open.

#28 In alexkeizer/QpfTypes;

· Equilibris opened on Jul 2, 2024

Feature: basic pattern matching for data-types

Status: Open.

#26 In alexkeizer/QpfTypes;

· alexkeizer opened on Jun 26, 2024

Remove PFin2 in favour of Fin(2) using ulift

Status: Open.

#20 In alexkeizer/QpfTypes;

· Equilibris opened on Jun 25, 2024

Cleanup: make examples checked by CI

Status: Open.

#17 In alexkeizer/QpfTypes;

· alexkeizer opened on Jun 17, 2024

Feature: Introduce explicit syntax to distinguish live and dead variables

good first issueGood for newcomersGood for newcomers

Status: Open.

#16 In alexkeizer/QpfTypes;

· alexkeizer opened on Jun 4, 2024

Feature: Accept some form of type ascriptions on <code>data</code> and <code>codata</code>

Status: Open.

#15 In alexkeizer/QpfTypes;

· alexkeizer opened on May 23, 2024

Cleanup: Consistent Code Formatting

Status: Open.

#12 In alexkeizer/QpfTypes;

· alexkeizer opened on May 20, 2024

Cleanup: get rid of noisy lines (e.g., <code>#check</code>)

Status: Open.

#10 In alexkeizer/QpfTypes;

· alexkeizer opened on May 17, 2024

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

Status: Open.

#4 In alexkeizer/QpfTypes;

· alexkeizer opened on Feb 17, 2024