Issues - 1lab/mikan - Codeberg.org

This website requires JavaScript.

1lab/mikan

1lab/mikan

Code Issues 25 Pull requests 4 Projects 1 Activity

Labels Milestones

Search syntax

`assignee:<username>`	Filter by assigned user
`author:<username>`	Filter by the author
`is:all`	All
`is:closed`	Closed
`is:open`	Open
`mentions:<username>`	Filter by mentioned user
`modified:[>\|<]<date>`	Filter by last modified date
`review:<username>`	Filter by user who reviewed
`sort:<by>:[asc\|desc]`	Sort by: `created\|comments\|updated\|deadline`

New issue

25 Open 32 Closed 57 All

Label

Show archived labels

All labels No label

language change

A: highlighting

good first issue

Milestone

All milestones No milestones

Open milestones

Initial release

Project

All projects No project

Open projects

Diagnostic reporting revamp

Author

Assignee

All assignees No assignee amyliao ncf totbwf

Sort

Relevance Newest Oldest Recently updated Least recently updated Most commented Least commented Nearest due date Farthest due date

25 Open 32 Closed 57 All

Label

Clear labels

1 - scope

language

1 - scope

language change

1 - scope

performance

1 - scope

task

A: dead-code

A: errors

A: highlighting

A: imports

A: infra

A: instance

A: lhs

A: modules

A: parallel

A: positivity

A: printing

A: records

A: scoping

A: termination

0 - type

bug

0 - type

discussion

0 - type

question

9 - status

duplicate

9 - status

info needed

9 - status

invalid

good first issue

upstream

Milestone

No milestone

Open milestones

Initial release

Projects

Clear projects

Open projects

Diagnostic reporting revamp

Assignee

Clear assignees

No assignee

amyliao

ncf

totbwf

Clarify copattern translation/"constructor inlining"

language change

#148 opened 2026年06月30日 15:45:33 +02:00 by ncf 0 / 4

Panic when checking a DISPLAY pragma whose RHS involves a module parameter

good first issue

#135 opened 2026年06月12日 20:24:19 +02:00 by totbwf

Typechecking anonymous parametrized module is much slower than expected

#133 opened 2026年06月10日 18:38:17 +02:00 by jaycech3n

Turn "missing with-clauses" into a warning?

#124 opened 2026年05月28日 15:21:58 +02:00 by jeanas

Decide on a fate for non-uniform parameterised types

language change

#120 opened 2026年05月27日 17:03:59 +02:00 by amyliao

Lazier unSpineing of display forms for postfix projections

#109 opened 2026年05月19日 16:59:22 +02:00 by amyliao

Full support for Indexed Inductive-Recursive Types in Mikan

#105 opened 2026年05月19日 07:19:58 +02:00 by EmberEdison

CantResolveOverloadedConstructorsTargetingSameDatatype sometimes worse than useless

good first issue

#104 opened 2026年05月15日 18:30:36 +02:00 by amyliao Diagnostic reporting revamp

Move to diagnostic codes

#99 opened 2026年05月15日 16:18:49 +02:00 by amyliao Diagnostic reporting revamp

Diagnostic messages should not print back "input" abstract syntax

#98 opened 2026年05月15日 15:45:40 +02:00 by amyliao Diagnostic reporting revamp

CI: Check the 1Lab

#97 opened 2026年05月15日 15:35:35 +02:00 by amyliao

GHC plugin for lifting debug printing out-of-line

#93 opened 2026年05月14日 15:07:26 +02:00 by amyliao

Termination checking for mixed inductive/coinductive types performs quantifier inversion

#84 opened 2026年05月07日 23:26:25 +02:00 by totbwf

Make λ arguments always interpreted as patterns?

language change

#79 opened 2026年05月06日 00:00:33 +02:00 by jeanas

Add nice syntax for Σ types

language change

#78 opened 2026年05月05日 23:52:39 +02:00 by jeanas

Cubical term-building needlessly complex

#71 opened 2026年05月04日 15:20:12 +02:00 by amyliao

Remove -fexpose-all-unfoldings and -fspecialise-aggressively

#69 opened 2026年04月30日 18:35:40 +02:00 by totbwf

Style Guide

#61 opened 2026年04月29日 14:32:54 +02:00 by totbwf

Kan operations for Prop

#53 opened 2026年04月27日 16:28:06 +02:00 by totbwf

Port QuickCheck tests to hedgehog

#23 opened 2026年04月23日 20:30:37 +02:00 by totbwf

Add option that makes Agda output test-sanitized output

#18 opened 2026年04月22日 20:02:10 +02:00 by totbwf

Interaction Mode Wishlist

#17 opened 2026年04月22日 18:42:08 +02:00 by totbwf

Build system simplification

#4 opened 2026年04月20日 14:30:36 +02:00 by amyliao 2 / 3

Documentation

#3 opened 2026年04月20日 14:24:22 +02:00 by amyliao Initial release

Post-fork language consolidation

language change

#1 opened 2026年04月20日 14:19:10 +02:00 by amyliao Initial release 21 / 24