1
0
Fork
You've already forked mikan
0
forked from 1lab/mikan
No description
  • Haskell 56.5%
  • Agda 25.9%
  • TeX 6.9%
  • PostScript 4%
  • HTML 3.2%
  • Other 3.4%
Reed Mullanix 002a1120fd fix: port interaction tests ( #16 ) 
This PR pulls the nightmare sed script in `test/interaction/Makefile`
into a Haskell DSL, and also ports all of the interaction tests to cabal
tests. I've also moved all of the tests from `test/interaction` to
`tests/Interaction` to align with the other cabal-based tests, hence the
thousands of files changed.
This closes #12.
Reviewed-on: 1lab/mikan#16
2026年04月23日 17:34:06 +02:00
.vscode Re #7065 : Remove .vscode/settings.json from version control again 2024年02月13日 08:10:48 +01:00
.woodpecker chore: only build on push events on main 2026年04月21日 22:59:59 -03:00
benchmark makefile: ban whichcraft 2026年02月11日 12:13:49 +01:00
cubical @fe3394eba7 Update std-lib and cubical submodules 2026年04月18日 17:16:36 +02:00
doc chore: remove sized-types tests 2026年04月22日 19:36:01 +02:00
examples Reverted two commits that made certain level arguments erased. 2026年03月17日 10:35:48 +01:00
mk use mikan not agda 2026年04月20日 14:53:31 +00:00
notes Disable the size-solver-test 2025年03月06日 19:27:38 +01:00
src fix: port interaction tests ( #16 ) 2026年04月23日 17:34:06 +02:00
test fix: port interaction tests ( #16 ) 2026年04月23日 17:34:06 +02:00
.editorconfig Add an EditorConfig file 2026年02月25日 15:06:39 +01:00
.gitignore Fix nix build, get all tests running, and use nix for our CI ( #11 ) 2026年04月21日 17:39:50 +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
.readthedocs.yaml readthedocs.org now needs a configuration file 2023年05月05日 17:37:45 +02:00
cabal.project Fix nix build, get all tests running, and use nix for our CI ( #11 ) 2026年04月21日 17:39:50 +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.local.mtl23 Fix #6283 : build with mtl-2.3.1 2022年11月04日 09:01:12 +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
CITATION.cff Bump Agda version to 2.9.0 2025年07月05日 22:50:22 +02:00
CODE_OF_CONDUCT.md chore: start rebranding 2026年04月20日 08:43:29 -03:00
CONTRIBUTING.md chore: start rebranding 2026年04月20日 08:43:29 -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 fix: use HLS for the correct GHC version 2026年04月22日 14:09:25 +02:00
HACKING.md Fix nix build, get all tests running, and use nix for our CI ( #11 ) 2026年04月21日 17:39:50 +02:00
LICENSE chore: start rebranding 2026年04月20日 08:43:29 -03:00
Makefile chore: remove sized-types tests 2026年04月22日 19:36:01 +02:00
Mikan.cabal fix: port interaction tests ( #16 ) 2026年04月23日 17:34:06 +02:00
README.md chore: start rebranding 2026年04月20日 08:43:29 -03:00
release.sh Fix release.sh: prevent the masking of a return value 2023年09月24日 17:10:33 +02:00
touchup.sh Refactoring guided by hlint ( #4479 ) 2020年03月18日 14:08:32 +01: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.