1
0
Fork
You've already forked mikan
0
forked from 1lab/mikan
No description
  • Haskell 60.5%
  • Agda 26.8%
  • TeX 5.4%
  • HTML 4%
  • Emacs Lisp 1.9%
  • Other 1.4%
Amélia Liao 5fd3212d21
 fix: forbid anything with DotP subpatterns 
Minor revision to #118 which adds any patterns that *contain* DotPs
(instead of *being* DotPs) to the forbidden variable set. This guards
against a revision of @ncf's minimal reproducer where the problematic
substitution of WOne for X happens under a box (either inductive or
record).
2026年05月27日 13:20:22 -03:00
.woodpecker ci: use add instead of install 2026年05月02日 15:13:38 +02:00
benchmark rename Set to Type 2026年05月27日 16:57:02 +02:00
cubical @fe3394eba7 Update std-lib and cubical submodules 2026年04月18日 17:16:36 +02:00
doc rename Set to Type 2026年05月27日 16:57:02 +02:00
mk chore: remove more references to stack 2026年04月26日 00:18:59 -04:00
notes Remove modalities 2026年05月10日 01:06:02 +02:00
src fix: forbid anything with DotP subpatterns 2026年05月27日 13:20:22 -03:00
test fix: forbid anything with DotP subpatterns 2026年05月27日 13:20:22 -03:00
.editorconfig Add an EditorConfig file 2026年02月25日 15:06:39 +01:00
.gitignore Remove modalities 2026年05月10日 01:06:02 +02:00
.gitmodules chore: remove stdlib 2026年04月21日 22:46:37 -03:00
.hlint.yaml Follow hlint suggestion: redundant case 2024年08月16日 18:06:43 +02:00
.mailmap Update .mailmap 2025年04月07日 13:58:03 +02:00
cabal.project fix: pull mikan-bisect back out into cabal file 2026年04月29日 00:09:45 +02:00
cabal.project.ghc-9.14.1 [workflows] add Cabal GHC 9.14, reactivate cubical [wasm] 2026年02月04日 20:40:53 +01:00
cabal.project.tc chore: start rebranding 2026年04月20日 08:43:29 -03:00
CHANGELOG.md Bump CI to GHC 9.14.1 2026年04月18日 17:16:36 +02:00
CODE_OF_CONDUCT.md chore: start rebranding 2026年04月20日 08:43:29 -03:00
CONTRIBUTING.md chore: slice off rest of CONTRIBUTING.md 2026年04月24日 21:22:35 -03:00
fix-whitespace.yaml Add *.agda-lib to fix-whitespace.yaml 2025年06月30日 17:10:37 +02:00
flake.lock nix: bump nixpkgs 2026年01月09日 14:12:29 +01:00
flake.nix chore: more rebranding 2026年05月21日 15:35:29 +02:00
HACKING.md chore: more rebranding 2026年05月21日 15:35:29 +02:00
LICENSE chore: relicense, but properly 2026年04月28日 21:12:35 -03:00
Makefile chore: remove examples/ 2026年04月28日 20:45:36 +02:00
Mikan.cabal Documentation fixes and dead code removal ( #60 ) 2026年05月25日 19:40:31 +02:00
README.md Link to the announcement from the README 2026年05月19日 14:10:26 +02:00
weeder.toml Remove global and local rewrite rules ( #68 ) 2026年05月04日 18:18:18 +02:00

Mikan logo & header

Mikan (Citrus unshiu) is a proof assistant for De Morgan cubical type theory, forked from Agda just before the release of version 2.9.0, and maintained by the 1Lab development team.

To learn more about the motivations for the fork and the direction of the project, read the Mikan announcement post, in particular the frequently asked questions.