Agda 2

Settings | Report Duplicate

1

I Use This!

High Activity

Commits : Listings

Analyzed about 24 hours ago. based on code collected 2 days ago.

Commit Message	Contributor	Files Modified	Lines Added	Lines Removed	Code Location	Date
Aug 29, 2025 — Aug 29, 2026 Showing page 1 of 808 Search / Filter on:
Fix #8697 by indexing the memo map for Double by their Word64 representation	Andreas Abel	More...				2 days ago
Fix #8699 (irr) by not going into irrelevant subterms in dot patterns	Andreas Abel	More...				2 days ago
Cosmetics: use unlessM	Andreas Abel	More...				2 days ago
Allow irrelevant dot patterns, because they are allowed for Prop	Andreas Abel	More...				3 days ago
Testsuite: we were missing a test for irrelevant garbage dot patterns	Andreas Abel	More...				3 days ago
Fix #8699 (Prop): dot-pattern termination: don't count descent under DontCare	Andreas Abel	More...				3 days ago
[ fix #8700 ] Do not consider definitions with missing clauses or hcomp applications as matchable for clause-based matcher	Jesper Cockx	More...				3 days ago
[ debug ] Improve debug printing for clause-based matcher	Jesper Cockx	More...				3 days ago
Refactor: store information isPathCons at constructor rather than datatype	Andreas Abel	More...				3 days ago
[ fix #8694 ] Take relevance into account for cycle rule in LHS unifier (#8702)	Jesper Cockx	More...				3 days ago
Fix #8687 by computing the checkpoints more directly and postponing `unsafeInTopContext`	Andreas Abel	More...				4 days ago
[comment] Document the fields of the PiSort constructor	Andreas Abel	More...				4 days ago
Re #8688: occurrences: descend covariantly into `Sort s` with --cumulativity	Andreas Abel	More...				4 days ago
Fix #8688: positivity checker now also descends into `Sort s`	Andreas Abel	More...				4 days ago
Refactor ProjectionLike: fuse validProj into candidateArgs	Andreas Abel	More...				5 days ago
Fix #8686 (2): projection-like: apply reduceDefCopy on domain of principal argument	Andreas Abel	More...				5 days ago
Fix #8686 (1): projection-like: disallow irrelevant parameters in principal arg	Andreas Abel	More...				5 days ago
Fix #8683: check cubical side conditions also in inference mode	Andreas Abel	More...				6 days ago
Fix #8680 (pattern syn) by removing spurious `__IMPOSSIBLE__`	Andreas Abel	More...				7 days ago
Change R.constructor so that R is the record module rather than the type	Andreas Abel	More...				7 days ago
Fix #7564: Do not crash when trying eta-contraction on over-applied constructor.	Andreas Abel	More...				8 days ago
[ fix #5665 ] Close information gaps in the JSON interaction protocol	willtunnels	More...				9 days ago
Fix #8599: classifyPattern: in ordinary patterns can't be copatterns	Andreas Abel	More...				10 days ago
Re #8599: fix rendering of error message: invert -> with	Andreas Abel	More...				10 days ago
Fix #8674 by inserting missing inConcreteOrAbstractMode	Andreas Abel	More...				10 days ago
Dead code elimination: skip meta judgement types unless --save-metas	Valerii Huhnin	More...				11 days ago
[ re #8638 ] qualified import of Data.List	Jesper Cockx	More...				11 days ago
[ fix #8609 ] Move debug print to inside withBranchState call	Jesper Cockx	More...				11 days ago
[ re #8638 ] Rename etaRecordSplits -> lazySplits in coverage checker	Jesper Cockx	More...				11 days ago
Relax base bound for cifm	Andreas Abel	More...				11 days ago

←
1
2
3
4
5
6
7
8
9
…
807
808
→