Agda is now a self-contained single binary.
Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
Experimental support for polarity annotations with new flag --polarity.
Compile to JavaScript with ES6 module syntax with new flag --js-es6.
Errors now have an identifier and follow the GNU standard.
Dropped support for GHC 8.6, added support for GHC 9.12.
Agda supports GHC versions 8.8.4 to 9.12.2.
The agda binary now contains everything to set itself up,
it need not be shipped with additional files.
The functionality of the agda-mode executable has been replicated
under the new option --emacs-mode.
The agda-mode executable is now deprecated.
References to agda-mode in your .emacs file should be replaced
by agda --emacs-mode.
Agda now contains all its data files,
like primitive and builtin modules,
supplements for the HTML and LaTeX backends,
the runtimes for the JS and GHC backends,
and the emacs mode.
These will be written to the data directory
on the first invocation of agda or an invocation ofagda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
The location of the data directory can be printed usingagda --print-agda-data-dir and can be controlled by the use-xdg-data-home
flag at build time and the Agda_datadir environment variable at runtime; see the
documentation for more information.
The Cabal/Stack custom installation Setup.hs has been removed
that previously generated the .agdai files for the builtin and primitive modules.
These will now be generated by Agda whenever they are needed,
just as for ordinary modules.
This change might be breaking for packagers of Agda
as the packaging routines might need to be updated: in particular,
declarative build systems like Nix or Guix should generate the .agdai files
by invoking Agda at build time.
Pre-built binaries are available as release assets for the following platforms
Installation instructions are provided in the Agda user manual.
The optimise-heavily build flag is now turned on by default.
This requires more resources when building Agda, but leads to a faster Agda binary.
Should GHC run out of memory when building Agda, turn this flag off.
Added cabal build flag dump-core to save the optimised GHC Core code during
compilation of Agda. This can be useful for people working on improving the
performance of the Agda implementation.
BREAKING: Abbreviation of options, such as --warning to --warn, is no longer supported.
New main mode of operation --build-library (issue #4338).
Invoking agda --build-library will look for an .agda-lib file starting in the current directory.
It will then extract the include directories of this library,
collect all Agda files in these directories and their subdirectories,
and check all these files.
New option --setup that writes out the Agda data files (see above)
and can be used to regenerate them.
New option --emacs-mode to administer the Emacs mode
as previously done by the agda-mode executable.
Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.
New option --js-es6 for generating JavaScript with ES6 module syntax.
DISPLAY pragmas can now define display forms that match on defined names
beyond constructors (issue #7533).
Example:
{-# DISPLAY Irrelevant Empty = ⊥ #-}
Empty used to be interpreted as a pattern variable, effectively installing
the display form Irrelevant _ = ⊥.
Now Empty is treated as a matchable name, as one would intuitively expect
from a display form.
As a consequence, only Irrelevant Empty is displayed as ⊥, not just anyIrrelevant A.
A new experimental flag --experimental-lazy-instances causes
instance selection to be deferred until the type of the instance
constraint is determined enough to make an unamibiguous decision at
the discrimination tree level. This significantly improves performance
for cases where instances can be distinguished by rigid data.
This flag will become the default in the future, but it is currently
disabled by default because it has unexpected interactions with
parts of the codebase (and macros) which rely on constraint solving
order (see e.g. issue #7882
and issue #7847).
New warning RewritesNothing if a rewrite clause did not fire.
New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance
when wrong user-written attribute was corrected automatically by Agda.
New deadcode warning InvalidDisplayForm instead of hard error
when a display form is illegal (and thus ignored).
New warning UnusedVariablesInDisplayForm when DISPLAY pragma
binds variables that are not used.
Example:
{-# DISPLAY List (Fin n) = ListFin #-}
Since pattern variable n is not used on the right hand side ListFin,
Agda throws a warning and recommeds to rewrite it as:
{-# DISPLAY List (Fin _) = ListFin #-}Unused CATCHALL pragmas now trigger UselessPragma warnings.
New deadcode warning EmptyPolarityPragma for POLARITY pragma without polarities.
E.g. triggered by {-# POLARITY F #-}.
New parser warnings MisplacedAttributes, UnknownAttribute, and UnknownPolarity
instead of hard parser errors.
New deadcode warning TooManyPolarities instead of hard error
when a POLARITY pragma gives polarities that exceed the known
arity of the postulate.
New deadcode warning UselessTactic when a @tactic attribute has no effect,
typically when it is attached to a non-hidden or instance argument.
New warning WithClauseProjectionFixityMismatch instead of hard error
when in a with-clause a projection is used in a different fixity
(prefix vs. postfix) than in its parent clause.
New error warning TooManyArgumentsToSort instead of hard error.
Warning AbsurdPatternRequiresNoRHS has been renamed toAbsurdPatternRequiresAbsentRHS.
Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced
by new warnings OpenImportAbstract and OpenImportPrivate.
Warning NoGuardednessFlag has been removed.
Instead Agda gives a hint when --guardedness would help with termination checking,
unless options --sized-types or --no-guardedness are set.
Support for polarity annotations can be enabled by the feature flag--polarity.
This flag is infective.
Uses of variables bound with polarity annotations are checked through modal
typing rules, and the positivity checker has been expanded to take annotations
into account. This means that the following is now definable:
{-# OPTIONS --polarity #-}
data Mu (F : @++ Set → Set) : Set where
fix : F (Mu F) → Mu FAdditions to the Agda syntax.
Add new literate agda: forester, see #7403.
You will need the postprocessor agda-tree,
see Agda user manual on literate programming for more information.
It is now always possible to refer to the name of a record type's
constructor, even if a name was not explicitly specified. This is done
using the new (Record name).constructor syntax;
see issue #6964 for the motivation.
The left-hand-sides of functions bound in a let expression can now
contain the same types of patterns that are allowed in lambda
expressions, in dependent function types, and in other let bindings.
This means that
let f : A → B → C f p1 p2 = ... in ...
should be accepted exactly when, and have the same meaning as,
let f : A → B → C f = λ p1 p2 → ...
See #7572.
Changes to type checker and other components defining the Agda language.
BREAKING: The primitive "cubical identity type", previously
exported from Agda.Builtin.Cubical.Id, has been removed. Its
computational behaviour is exactly replicated by the user-definable
identity type, which is also exported from Agda.Builtin.Equality.
See agda/cubical#1005 for
the PR removing it from the library, and
#7652 for the compiler.
Inlining constructors no longer happens on the right-hand-sides ofINLINE functions. This allows using INLINE functions to define
"smart constructors" for record types which have the same reduction
behaviour as using the actual constructor would. Small example:
triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }
ex = triple 1 2 3
Here, constructor inlining happens on the right hand side of ex
rather than of triple.
Changes to the meta-programming facilities.
New reflection primitive: checkFromStringTC : String → Type → TC Term
Parse and ty...
Agda is now a self-contained single binary.
Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
Experimental support for polarity annotations with new flag --polarity.
Compile to JavaScript with ES6 module syntax with new flag --js-es6.
Errors now have an identifier and follow the GNU standard.
The optimise-heavily build flag is now turned on by default.
Dropped support for GHC 8.6, added support for GHC 9.12.
Agda supports GHC versions 8.8.4 to 9.12.2.
The agda binary now contains everything to set itself up,
it need not be shipped with additional files.
The functionality of the agda-mode executable has been replicated
under the new option --emacs-mode.
The agda-mode executable is now deprecated.
References to agda-mode in your .emacs file should be replaced
by agda --emacs-mode.
Agda now contains all its data files,
like primitive and builtin modules,
supplements for the HTML and LaTeX backends,
the runtimes for the JS and GHC backends,
and the emacs mode.
These will be written to ${Agda_datadir}/${VERSION}
on the first invocation of agda or an invocation ofagda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
Herein, ${VERSION} is the Agda version and ${Agda_datadir}
the Agda data directory, on Unix-like systems
defaulting to ${HOME}/.local/share/agda.
The Cabal/Stack custom installation Setup.hs has been removed
that previously generated the .agdai files for the builtin and primitive modules.
These will now be generated by Agda whenever they are needed,
just as for ordinary modules.
This change is breaking for packagers of Agda
as the packaging routines might need to be updated
(but should become simpler).
Added cabal build flag dump-core to save the optimised GHC Core code during
compilation of Agda. This can be useful for people working on improving the
performance of the Agda implementation.
New main mode of operation --build-library (issue #4338).
Invoking agda --build-library will look for an .agda-lib file starting in the current directory.
It will then extract the include directories of this library,
collect all Agda files in these directories and their subdirectories,
and check all these files.
New option --setup that writes out the Agda data files (see above)
and can be used to regenerate them.
New option --emacs-mode to administer the Emacs mode
as previously done by the agda-mode executable.
Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.
New option --js-es6 for generating JavaScript with ES6 module syntax.
DISPLAY pragmas can now define display forms that match on defined names
beyond constructors (issue #7533).
Example:
{-# DISPLAY Irrelevant Empty = ⊥ #-}
Empty used to be interpreted as a pattern variable, effectively installing
the display form Irrelevant _ = ⊥.
Now Empty is treated as a matchable name, as one would intuitively expect
from a display form.
As a consequence, only Irrelevant Empty is displayed as ⊥, not just anyIrrelevant A.
A new experimental flag --experimental-lazy-instances causes
instance selection to be deferred until the type of the instance
constraint is determined enough to make an unamibiguous decision at
the discrimination tree level. This significantly improves performance
for cases where instances can be distinguished by rigid data.
This flag will become the default in the future, but it is currently
disabled by default because it has unexpected interactions with
parts of the codebase (and macros) which rely on constraint solving
order (see e.g. issue #7882
and issue #7847).
New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance
when wrong user-written attribute was corrected automatically by Agda.
New deadcode warning InvalidDisplayForm instead of hard error
when a display form is illegal (and thus ignored).
New warning UnusedVariablesInDisplayForm when DISPLAY pragma
binds variables that are not used.
Example:
{-# DISPLAY List (Fin n) = ListFin #-}
Since pattern variable n is not used on the right hand side ListFin,
Agda throws a warning and recommeds to rewrite it as:
{-# DISPLAY List (Fin _) = ListFin #-}Unused CATCHALL pragmas now trigger UselessPragma warnings.
New deadcode warning EmptyPolarityPragma for POLARITY pragma without polarities.
E.g. triggered by {-# POLARITY F #-}.
New deadcode warning TooManyPolarities instead of hard error
when a POLARITY pragma gives polarities that exceed the known
arity of the postulate.
New deadcode warning UselessTactic when a @tactic attribute has no effect,
typically when it is attached to a non-hidden or instance argument.
New warning WithClauseProjectionFixityMismatch instead of hard error
when in a with-clause a projection is used in a different fixity
(prefix vs. postfix) than in its parent clause.
New error warning TooManyArgumentsToSort instead of hard error.
Warning AbsurdPatternRequiresNoRHS has been renamed toAbsurdPatternRequiresAbsentRHS.
Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced
by new warnings OpenImportAbstract and OpenImportPrivate.
Warning NoGuardednessFlag has been removed.
Instead Agda gives a hint when --guardedness would help with termination checking,
unless options --sized-types or --no-guardedness are set.
Support for polarity annotations can be enabled by the feature flag--polarity.
This flag is infective.
Uses of variables bound with polarity annotations are checked through modal
typing rules, and the positivity checker has been expanded to take annotations
into account. This means that the following is now definable:
{-# OPTIONS --polarity #-}
data Mu (F : @++ Set → Set) : Set where
fix : F (Mu F) → Mu FAdditions to the Agda syntax.
Add new literate agda: forester, see #7403.
You will need the postprocessor agda-tree, see Agda user manual on literate programming for more information.
It is now always possible to refer to the name of a record type's
constructor, even if a name was not explicitly specified. This is done
using the new (Record name).constructor syntax; See issue
#6964 for the motivation.
The left-hand-sides of functions bound in a let expression can now
contain the same types of patterns that are allowed in lambda
expressions, in dependent function types, and in other let bindings.
This means that
let f : A → B → C f p1 p2 = ... in ...
should be accepted exactly when, and have the same meaning as,
let f : A → B → C f = λ p1 p2 → ...
See #7572.
Changes to type checker and other components defining the Agda language.
BREAKING: The primitive "cubical identity type", previously
exported from Agda.Builtin.Cubical.Id, has been removed. Its
computational behaviour is exactly replicated by the user-definable
identity type, which is also exported from Agda.Builtin.Equality.
See agda/cubical#1005 for
the PR removing it from the library, and
#7652 for the compiler.
Inlining constructors no longer happens on the right-hand-sides ofINLINE functions. This allows using INLINE functions to define
"smart constructors" for record types which have the same reduction
behaviour as using the actual constructor would. Small example:
triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }
ex = triple 1 2 3
Here, constructor inlining happens on the right hand side of ex
rather than of triple.
Changes to the meta-programming facilities.
New reflection primitive: checkFromStringTC : String → Type → TC Term
Parse and type check the given string against the given type, returning
the resulting term (when successful).
.agda-lib files in the rootAgda's error messages now follow the GNU standard.
To comply with this policy, line and column are now separated by a dot instead of comma.
The format of regular errors and error warnings follows this template:
sourcefile:line1.column1-line2.column2: error: [ErrorName]
...
error message
...
when error context
line2 or even column2 can be missing, in some cases even the entire error location.
I...
Agda is now a self-contained single binary.
Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
Experimental support for polarity annotations with new flag --polarity.
Compile to JavaScript with ES6 module syntax with new flag --js-es6.
Errors now have an identifier and follow the GNU standard.
Dropped support for GHC 8.6, added support for GHC 9.12.
Agda supports GHC versions 8.8.4 to 9.12.2.
The agda binary now contains everything to set itself up,
it need not be shipped with additional files.
The functionality of the agda-mode executable has been replicated
under the new option --emacs-mode.
The agda-mode executable is now deprecated.
References to agda-mode in your .emacs file should be replaced
by agda --emacs-mode.
Agda now contains all its data files,
like primitive and builtin modules,
supplements for the HTML and LaTeX backends,
the runtimes for the JS and GHC backends,
and the emacs mode.
These will be written to ${Agda_datadir}/${VERSION}
on the first invocation of agda or an invocation ofagda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
Herein, ${VERSION} is the Agda version and ${Agda_datadir}
the Agda data directory, on Unix-like systems
defaulting to ${HOME}/.local/share/agda.
The Cabal/Stack custom installation Setup.hs has been removed
that previously generated the .agdai files for the builtin and primitive modules.
These will now be generated by Agda whenever they are needed,
just as for ordinary modules.
This change is breaking for packagers of Agda
as the packaging routines might need to be updated
(but should become simpler).
Added cabal build flag dump-core to save the optimised GHC Core code during
compilation of Agda. This can be useful for people working on improving the
performance of the Agda implementation.
New main mode of operation --build-library (issue #4338).
Invoking agda --build-library will look for an .agda-lib file starting in the current directory.
It will then extract the include directories of this library,
collect all Agda files in these directories and their subdirectories,
and check all these files.
New option --setup that writes out the Agda data files (see above)
and can be used to regenerate them.
New option --emacs-mode to administer the Emacs mode
as previously done by the agda-mode executable.
Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.
New option --js-es6 for generating JavaScript with ES6 module syntax.
DISPLAY pragmas can now define display forms that match on defined names
beyond constructors (issue #7533).
Example:
{-# DISPLAY Irrelevant Empty = ⊥ #-}
Empty used to be interpreted as a pattern variable, effectively installing
the display form Irrelevant _ = ⊥.
Now Empty is treated as a matchable name, as one would intuitively expect
from a display form.
As a consequence, only Irrelevant Empty is displayed as ⊥, not just anyIrrelevant A.
A new experimental flag --experimental-lazy-instances causes
instance selection to be deferred until the type of the instance
constraint is determined enough to make an unamibiguous decision at
the discrimination tree level. This significantly improves performance
for cases where instances can be distinguished by rigid data.
This flag will become the default in the future, but it is currently
disabled by default because it has unexpected interactions with
parts of the codebase (and macros) which rely on constraint solving
order (see e.g. issue #7882
and issue #7847).
New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance
when wrong user-written attribute was corrected automatically by Agda.
New deadcode warning InvalidDisplayForm instead of hard error
when a display form is illegal (and thus ignored).
New warning UnusedVariablesInDisplayForm when DISPLAY pragma
binds variables that are not used.
Example:
{-# DISPLAY List (Fin n) = ListFin #-}
Since pattern variable n is not used on the right hand side ListFin,
Agda throws a warning and recommeds to rewrite it as:
{-# DISPLAY List (Fin _) = ListFin #-}Unused CATCHALL pragmas now trigger UselessPragma warnings.
New deadcode warning EmptyPolarityPragma for POLARITY pragma without polarities.
E.g. triggered by {-# POLARITY F #-}.
New deadcode warning TooManyPolarities instead of hard error
when a POLARITY pragma gives polarities that exceed the known
arity of the postulate.
New deadcode warning UselessTactic when a @tactic attribute has no effect,
typically when it is attached to a non-hidden or instance argument.
New warning WithClauseProjectionFixityMismatch instead of hard error
when in a with-clause a projection is used in a different fixity
(prefix vs. postfix) than in its parent clause.
New error warning TooManyArgumentsToSort instead of hard error.
Warning AbsurdPatternRequiresNoRHS has been renamed toAbsurdPatternRequiresAbsentRHS.
Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced
by new warnings OpenImportAbstract and OpenImportPrivate.
Warning NoGuardednessFlag has been removed.
Instead Agda gives a hint when --guardedness would help with termination checking,
unless options --sized-types or --no-guardedness are set.
Support for polarity annotations can be enabled by the feature flag--polarity.
This flag is infective.
Uses of variables bound with polarity annotations are checked through modal
typing rules, and the positivity checker has been expanded to take annotations
into account. This means that the following is now definable:
{-# OPTIONS --polarity #-}
data Mu (F : @++ Set → Set) : Set where
fix : F (Mu F) → Mu FAdditions to the Agda syntax.
Add new literate agda: forester, see #7403.
You will need the postprocessor agda-tree, see Agda user manual on literate programming for more information.
It is now always possible to refer to the name of a record type's
constructor, even if a name was not explicitly specified. This is done
using the new (Record name).constructor syntax; See issue
#6964 for the motivation.
The left-hand-sides of functions bound in a let expression can now
contain the same types of patterns that are allowed in lambda
expressions, in dependent function types, and in other let bindings.
This means that
let f : A → B → C f p1 p2 = ... in ...
should be accepted exactly when, and have the same meaning as,
let f : A → B → C f = λ p1 p2 → ...
See #7572.
Changes to type checker and other components defining the Agda language.
BREAKING: The primitive "cubical identity type", previously
exported from Agda.Builtin.Cubical.Id, has been removed. Its
computational behaviour is exactly replicated by the user-definable
identity type, which is also exported from Agda.Builtin.Equality.
See agda/cubical#1005 for
the PR removing it from the library, and
#7652 for the compiler.
Inlining constructors no longer happens on the right-hand-sides ofINLINE functions. This allows using INLINE functions to define
"smart constructors" for record types which have the same reduction
behaviour as using the actual constructor would. Small example:
triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }
ex = triple 1 2 3
Here, constructor inlining happens on the right hand side of ex
rather than of triple.
Changes to the meta-programming facilities.
New reflection primitive: checkFromStringTC : String → Type → TC Term
Parse and type check the given string against the given type, returning
the resulting term (when successful).
.agda-lib files in the rootAgda's error messages now follow the GNU standard.
To comply with this policy, line and column are now separated by a dot instead of comma.
The format of regular errors and error warnings follows this template:
sourcefile:line1.column1-line2.column2: error: [ErrorName]
...
error message
...
when error context
line2 or even column2 can be missing, in some cases even the entire error location.
Internal errors might follow a different format.
Warnings are pr...
Agda is now a self-contained single binary.
Build all Agda files reachable from paths in the .agda-lib file with new flag --build-library.
Experimental support for polarity annotations with new flag --polarity.
Compile to JavaScript with ES6 module syntax with new flag --js-es6.
Errors now have an identifier and follow the GNU standard.
Dropped support for GHC 8.6, added support for GHC 9.12.
Agda supports GHC versions 8.8.4 to 9.12.2.
The agda binary now contains everything to set itself up,
it need not be shipped with additional files.
The functionality of the agda-mode executable has been replicated
under the new option --emacs-mode.
The agda-mode executable is now deprecated.
References to agda-mode in your .emacs file should be replaced
by agda --emacs-mode.
Agda now contains all its data files,
like primitive and builtin modules,
supplements for the HTML and LaTeX backends,
the runtimes for the JS and GHC backends,
and the emacs mode.
These will be written to ${Agda_datadir}/${VERSION}
on the first invocation of agda or an invocation ofagda --setup, agda --emacs-mode setup, or agda --emacs-mode compile.
Herein, ${VERSION} is the Agda version and ${Agda_datadir}
the Agda data directory, on Unix-like systems
defaulting to ${HOME}/.local/share/agda.
The Cabal/Stack custom installation Setup.hs has been removed
that previously generated the .agdai files for the builtin and primitive modules.
These will now be generated by Agda whenever they are needed,
just as for ordinary modules.
This change is breaking for packagers of Agda
as the packaging routines might need to be updated
(but should become simpler).
Added cabal build flag dump-core to save the optimised GHC Core code during
compilation of Agda. This can be useful for people working on improving the
performance of the Agda implementation.
New main mode of operation --build-library (issue #4338).
Invoking agda --build-library will look for an .agda-lib file starting in the current directory.
It will then extract the include directories of this library,
collect all Agda files in these directories and their subdirectories,
and check all these files.
New option --setup that writes out the Agda data files (see above)
and can be used to regenerate them.
New option --emacs-mode to administer the Emacs mode
as previously done by the agda-mode executable.
Option --local-interfaces and warning DuplicateInterfaceFiles have been removed.
New option --js-es6 for generating JavaScript with ES6 module syntax.
DISPLAY pragmas can now define display forms that match on defined names
beyond constructors (issue #7533).
Example:
{-# DISPLAY Irrelevant Empty = ⊥ #-}
Empty used to be interpreted as a pattern variable, effectively installing
the display form Irrelevant _ = ⊥.
Now Empty is treated as a matchable name, as one would intuitively expect
from a display form.
As a consequence, only Irrelevant Empty is displayed as ⊥, not just anyIrrelevant A.
New deadcode warnings FixingCohesion, FixingPolarity and FixingRelevance
when wrong user-written attribute was corrected automatically by Agda.
New deadcode warning InvalidDisplayForm instead of hard error
when a display form is illegal (and thus ignored).
New warning UnusedVariablesInDisplayForm when DISPLAY pragma
binds variables that are not used.
Example:
{-# DISPLAY List (Fin n) = ListFin #-}
Since pattern variable n is not used on the right hand side ListFin,
Agda throws a warning and recommeds to rewrite it as:
{-# DISPLAY List (Fin _) = ListFin #-}Unused CATCHALL pragmas now trigger UselessPragma warnings.
New deadcode warning EmptyPolarityPragma for POLARITY pragma without polarities.
E.g. triggered by {-# POLARITY F #-}.
New deadcode warning TooManyPolarities instead of hard error
when a POLARITY pragma gives polarities that exceed the known
arity of the postulate.
New deadcode warning UselessTactic when a @tactic attribute has no effect,
typically when it is attached to a non-hidden or instance argument.
New warning WithClauseProjectionFixityMismatch instead of hard error
when in a with-clause a projection is used in a different fixity
(prefix vs. postfix) than in its parent clause.
New error warning TooManyArgumentsToSort instead of hard error.
Warning AbsurdPatternRequiresNoRHS has been renamed toAbsurdPatternRequiresAbsentRHS.
Warnings OpenPublicAbstract and OpenPublicPrivate have been replaced
by new warnings OpenImportAbstract and OpenImportPrivate.
Warning NoGuardednessFlag has been removed.
Instead Agda gives a hint when --guardedness would help with termination checking,
unless options --sized-types or --no-guardedness are set.
Support for polarity annotations can be enabled by the feature flag--polarity.
This flag is infective.
Uses of variables bound with polarity annotations are checked through modal
typing rules, and the positivity checker has been expanded to take annotations
into account. This means that the following is now definable:
{-# OPTIONS --polarity #-}
data Mu (F : @++ Set → Set) : Set where
fix : F (Mu F) → Mu FAdditions to the Agda syntax.
Add new literate agda: forester, see #7403
It is now always possible to refer to the name of a record type's
constructor, even if a name was not explicitly specified. This is done
using the new (Record name).constructor syntax; See issue
#6964 for the motivation.
The left-hand-sides of functions bound in a let expression can now
contain the same types of patterns that are allowed in lambda
expressions, in dependent function types, and in other let bindings.
This means that
let f : A → B → C f p1 p2 = ... in ...
should be accepted exactly when, and have the same meaning as,
let f : A → B → C f = λ p1 p2 → ...
See #7572.
Changes to type checker and other components defining the Agda language.
BREAKING: The primitive "cubical identity type", previously
exported from Agda.Builtin.Cubical.Id, has been removed. Its
computational behaviour is exactly replicated by the user-definable
identity type, which is also exported from Agda.Builtin.Equality.
See agda/cubical#1005 for
the PR removing it from the library, and
#7652 for the compiler.
Inlining constructors no longer happens on the right-hand-sides ofINLINE functions. This allows using INLINE functions to define
"smart constructors" for record types which have the same reduction
behaviour as using the actual constructor would. Small example:
triple : Nat → Nat → Nat → Nat × Nat × Nat
{-# INLINE triple #-}
triple x y z = record { fst = x ; snd = y , z }
ex = triple 1 2 3
Here, constructor inlining happens on the right hand side of ex
rather than of triple.
Changes to the meta-programming facilities.
New reflection primitive: checkFromStringTC : String → Type → TC Term
Parse and type check the given string against the given type, returning
the resulting term (when successful).
.agda-lib files in the rootAgda's error messages now follow the GNU standard.
To comply with this policy, line and column are now separated by a dot instead of comma.
The format of regular errors and error warnings follows this template:
sourcefile:line1.column1-line2.column2: error: [ErrorName]
...
error message
...
when error context
line2 or even column2 can be missing, in some cases even the entire error location.
Internal errors might follow a different format.
Warnings are printed in a similar format:
sourcefile:line1.column1-line2.column2: warning: -W[no]WarningName
...
warning text
...
when warning context
Emacs: new face agda2-highlight-cosmetic-problem-face
for highlighting the new aspect CosmeticProblem.
Emacs: new face agda2-highlight-instance-problem-face
for highlighting the new aspect InstanceProblem.
When generating clauses after case splitting on a datatype defined in a parameterised module,
Agda now prints constructor names without a module prefix rather than fully qualified (see issue #3209).
This is only a surface-level fix, since Agda might still fail to find the properly qualified name for
the constructor in scope, but should at least make more sense in most situations.
New bindings for unicode 'tacks' (⟘⟙⟛⟝⟞⫫⫪) via \tack ...
This is a minor release of Agda fixing some bugs and regressions.
InstallationDuring installation, Agda type-checks its built-in modules and installs the generated .agdai files.
(This step is now skipped when the Agda executable is not installed, e.g. cabal install --lib Agda.)
Should the generation for (some of) these files fail, the names of the missing ones are now printed,
but installation continues nevertheless (PR #7465).
Rationale: installation of these files is only crucial when installing Agda in super-user mode.
Agda supports GHC versions 8.6.5 to 9.10.1.
The release notes of 2.7.0 claimed that the option --exact-split was now on by default
(Issue #7443).
This is actually not the case, the documentation has been suitably reverted.
Default option --save-metas has been reverted to --no-save-metas because of performance regressions
(Issue #7452).
Fixed an internal error related to interface files
(Issue #7436).
Fixed two internal errors in Mimer:
(Issue #7402 and
Issue #7484).
Fixed a regression causing needless re-checking of files
(Issue #7199).
Improved printing of terms by fixing a display form bug
(PR #7480).
For 2.7.0.1, the following issues were
closed
(see bug tracker):
--exact-split is not default in 2.7.0, contrary to claims--save-metas the defaultThese pull requests were merged for 2.7.0.1:
--no-save-metasFull Changelog: v2.7.0...v2.7.0.1
v2.7.0 Release notes for Agda version 2.7.0 HighlightsMimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.
New syntax using x ← e to bind values on the left-hand-side of a function clause.
Instance search is more performant thanks to a new indexing structure.
Additionally, users can now control how instances should be selected
in the case multiple candidates exist.
User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
are now on by default.
Agda versioning scheme switches to the Haskell Package Versioning Policy
so Agda can be more reliably used as a library.
Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...
When the creation of the Agda library interface files fails during installation,
a warning is emitted rather than aborting installation.
The absence of these interface files is not a problem if the Agda installation
resides in user space; they will be created on the fly then.
Yet for system-wide installations in root space or packaging,
the interface files should be created.
This can be achieved by a manual invocation of Agda on the library source files
(i.e., primitive and builtin modules Agda.*).
(See Issue #7401 and PR #7404.)
Agda supports GHC versions 8.6.5 to 9.10.1.
[Breaking] The option --overlapping-instances, which allows
backtracking during instance search, has been renamed to--backtracking-instance-search.
These options are now on by default:
--exact-split: Warn about clauses that are not definitional equalities.--keep-pattern-variables: Do not introduce dot patterns in interactive splitting.--postfix-projections: Print projections and projection patterns in postfix.--save-metas: Try to not unfold metavariable solutions in interface files.To revert to the old behavior, use options --no-....
Option --rewriting is now considered infective.
This means that if a module has this flag enabled,
then all modules importing it must also have that flag enabled.
New warnings:
CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
Used to be a hard error; now Agda continues, ignoring eta-equality.
ConflictingPragmaOptions if giving both --this and --that
when --this implies --no-that (and analogous for --no-this implies--that, etc).
ConstructorDoesNotFitInData when a constructor parameter
is too big (in the sense of universe level) for the target data type of the constructor.
Error warning, used to be a hard error.
DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
or declared inductive twice.
UselessMacro when a macro block does not contain any function definitions.
WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
Used to be a hard error.
Rejected rewrite rules no longer cause a hard error but instead cause
an error warning. The following warnings were added to document the
various reasons for rejection:
RewriteLHSNotDefinitionOrConstructorRewriteVariablesNotBoundByLHSRewriteVariablesBoundMoreThanOnceRewriteLHSReducesRewriteHeadSymbolIsProjectionRewriteHeadSymbolIsProjectionLikeFunctionRewriteHeadSymbolIsTypeConstructorRewriteHeadSymbolContainsMetasRewriteConstructorParametersNotGeneralRewriteContainsUnsolvedMetaVariablesRewriteBlockedOnProblemsRewriteRequiresDefinitionsRewriteDoesNotTargetRewriteRelationRewriteBeforeFunctionDefinitionRewriteBeforeMutualFunctionDefinitionNew option --require-unique-meta-solutions
(turned on by default).
Disabling it with --no-require-unique-meta-solutions allows the type checker
to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
The --lossy-unification flag implies --no-require-unique-meta-solutions.
New pragma INJECTIVE_FOR_INFERENCE
which treats functions as injective for inferring implicit arguments if--no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
file where the function is used, and not necessarily in the file where it is defined.
For example:
postulate
reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})
does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.
Additions to the Agda syntax.
Left-hand side let:using x ← e
(PR #7078)
This new construct can be use in left-hand sides together with with andrewrite to give names to subexpressions. It is the left-hand side
counterpart of a let-binding and supports the same limited form of pattern
matching on eta-expandable record values.
It can be quite useful when you have a function doing a series of nestedwiths that share some expressions. Something like
fun : A → B fun x using z ← e with foo z ... | p with bar z ... | q = r
Here the expression e doesn't have to be repeated in the two with-expressions.
As in a with, multiple bindings can be separated by a |, and variables to
the left are in scope in bindings to the right.
Pattern synonyms can now expose existing instance arguments
(PR 7173).
Example:
data D : Set where
c : {{D}} → D
pattern p {{d}} = c {{d}}
This allows us to explicitly bind these argument in a pattern match
and supply them explicitly when using the pattern synonym in an expression.
f : D → D
f (p {{d = x}}) = p {{d = x}}
We cannot create new instance arguments this way, though.
The following is rejected:
data D : Set where
c : D → D
pattern p {{d}} = c dChanges to type checker and other components defining the Agda language.
Agda now uses discrimination trees to store and look up instance
definitions, rather than linearly searching through all instances for
a given "class" (PR #7109).
This is a purely internal change, and should not result in any change
to which programs are accepted or rejected. However, it significantly
improves the performance of instance search, especially for the case
of a "type class" indexed by a single type argument. The new lookup
procedure should never be slower than the previous implementation.
Changes to the meta-programming facilities.
[Breaking] Erased constructors are now supported in reflection machinery.
Quantity argument was added to data-cons. For erased constructors this
argument has a value of quantity-0, otherwise it's quantity-ω.defineData now requires setting quantity for each constructor.
Add new primitive to run instance search from reflection code:
-- Try to solve open instance constraints. When wrapped in `noConstraints`, -- fails if there are unsolved instance constraints left over that originate -- from the current macro invokation. Outside constraints are still attempted, -- but failure to solve them are ignored by `noConstraints`. solveInstanceConstraints : TC ⊤
A new reflection primitive workOnTypes : TC A → TC A was added toAgda.Builtin.Reflection. This runs the given computation at the type level,
which enables the use of erased things. In particular, this is needed when
working with (dependent) function types with erased arguments. For example,
one can get the type of the tuple constructor _,_ (which now takes its type
parameters as erased arguments, see above) and unify it with the current goal
as follows:
macro testM : Term → TC ⊤ testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t)) typeOfComma = testM
[Breaking] The Auto command
Agsy has been replaced by an entirely new implementation Mimer
(PR #6410).
This fixes problems where Auto would fail in the presence of language features
it did not know about, such as copatterns or anything cubical.
The reimplementation does not support case splitting (-c), disproving
(-d) or refining (-r).
The Agda input method for Emacs has been extended by several character bindings.
The list of changes can be obtained with a git diff on the sources:
git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el
Highlighting some changes to Agda as a library.
Agda.Syntax.Common.KeywordRange providing type `KwRange...Reverted PR #5627 which had made options like --type-in-type infective.
Fixed issues #7382 (internal error in deserialization) and #7401 (cabal install --lib).
Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.
New syntax using x ← e to bind values on the left-hand-side of a function clause.
Instance search is more performant thanks to a new indexing structure.
Additionally, users can now control how instances should be selected
in the case multiple candidates exist.
User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
are now on by default.
Agda versioning scheme switches to the Haskell Package Versioning Policy
so Agda can be more reliably used as a library.
Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...
When the creation of the Agda library interface files fails during installation,
a warning is emitted rather than aborting installation.
The absence of these interface files is not a problem if the Agda installation
resides in user space; they will be created on the fly then.
Yet for system-wide installations in root space or packaging,
the interface files should be created.
This can be achieved by a manual invocation of Agda on the library source files
(i.e., primitive and builtin modules Agda.*).
(See Issue #7401 and PR #7404.)
Agda supports GHC versions 8.6.5 to 9.10.1.
[Breaking] The option --overlapping-instances, which allows
backtracking during instance search, has been renamed to--backtracking-instance-search.
These options are now on by default:
--exact-split: Warn about clauses that are not definitional equalities.--keep-pattern-variables: Do not introduce dot patterns in interactive splitting.--postfix-projections: Print projections and projection patterns in postfix.--save-metas: Try to not unfold metavariable solutions in interface files.To revert to the old behavior, use options --no-....
Option --rewriting is now considered infective.
This means that if a module has this flag enabled,
then all modules importing it must also have that flag enabled.
New warnings:
CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
Used to be a hard error; now Agda continues, ignoring eta-equality.
ConflictingPragmaOptions if giving both --this and --that
when --this implies --no-that (and analogous for --no-this implies--that, etc).
ConstructorDoesNotFitInData when a constructor parameter
is too big (in the sense of universe level) for the target data type of the constructor.
Error warning, used to be a hard error.
DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
or declared inductive twice.
UselessMacro when a macro block does not contain any function definitions.
WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
Used to be a hard error.
Rejected rewrite rules no longer cause a hard error but instead cause
an error warning. The following warnings were added to document the
various reasons for rejection:
RewriteLHSNotDefinitionOrConstructorRewriteVariablesNotBoundByLHSRewriteVariablesBoundMoreThanOnceRewriteLHSReducesRewriteHeadSymbolIsProjectionRewriteHeadSymbolIsProjectionLikeFunctionRewriteHeadSymbolIsTypeConstructorRewriteHeadSymbolContainsMetasRewriteConstructorParametersNotGeneralRewriteContainsUnsolvedMetaVariablesRewriteBlockedOnProblemsRewriteRequiresDefinitionsRewriteDoesNotTargetRewriteRelationRewriteBeforeFunctionDefinitionRewriteBeforeMutualFunctionDefinitionNew option --require-unique-meta-solutions
(turned on by default).
Disabling it with --no-require-unique-meta-solutions allows the type checker
to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
The --lossy-unification flag implies --no-require-unique-meta-solutions.
New pragma INJECTIVE_FOR_INFERENCE
which treats functions as injective for inferring implicit arguments if--no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
file where the function is used, and not necessarily in the file where it is defined.
For example:
postulate
reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})
does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.
Additions to the Agda syntax.
Left-hand side let:using x ← e
(PR #7078)
This new construct can be use in left-hand sides together with with andrewrite to give names to subexpressions. It is the left-hand side
counterpart of a let-binding and supports the same limited form of pattern
matching on eta-expandable record values.
It can be quite useful when you have a function doing a series of nestedwiths that share some expressions. Something like
fun : A → B fun x using z ← e with foo z ... | p with bar z ... | q = r
Here the expression e doesn't have to be repeated in the two with-expressions.
As in a with, multiple bindings can be separated by a |, and variables to
the left are in scope in bindings to the right.
Pattern synonyms can now expose existing instance arguments
(PR 7173).
Example:
data D : Set where
c : {{D}} → D
pattern p {{d}} = c {{d}}
This allows us to explicitly bind these argument in a pattern match
and supply them explicitly when using the pattern synonym in an expression.
f : D → D
f (p {{d = x}}) = p {{d = x}}
We cannot create new instance arguments this way, though.
The following is rejected:
data D : Set where
c : D → D
pattern p {{d}} = c dChanges to type checker and other components defining the Agda language.
Agda now uses discrimination trees to store and look up instance
definitions, rather than linearly searching through all instances for
a given "class" (PR #7109).
This is a purely internal change, and should not result in any change
to which programs are accepted or rejected. However, it significantly
improves the performance of instance search, especially for the case
of a "type class" indexed by a single type argument. The new lookup
procedure should never be slower than the previous implementation.
Changes to the meta-programming facilities.
[Breaking] Erased constructors are now supported in reflection machinery.
Quantity argument was added to data-cons. For erased constructors this
argument has a value of quantity-0, otherwise it's quantity-ω.defineData now requires setting quantity for each constructor.
Add new primitive to run instance search from reflection code:
-- Try to solve open instance constraints. When wrapped in `noConstraints`, -- fails if there are unsolved instance constraints left over that originate -- from the current macro invokation. Outside constraints are still attempted, -- but failure to solve them are ignored by `noConstraints`. solveInstanceConstraints : TC ⊤
A new reflection primitive workOnTypes : TC A → TC A was added toAgda.Builtin.Reflection. This runs the given computation at the type level,
which enables the use of erased things. In particular, this is needed when
working with (dependent) function types with erased arguments. For example,
one can get the type of the tuple constructor _,_ (which now takes its type
parameters as erased arguments, see above) and unify it with the current goal
as follows:
macro testM : Term → TC ⊤ testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t)) typeOfComma = testM
[Breaking] The Auto command
Agsy has been replaced by an entirely new implementation Mimer
(PR #6410).
This fixes problems where Auto would fail in the presence of language features
it did not know about, such as copatterns or anything cubical.
The reimplementation does not support case splitting (-c), disproving
(-d) or refining (-r).
The Agda input method for Emacs has been extended by several character bindings.
The lis...
Mimer, a re-implementation of the "auto" term synthesizer, replaces Agsy.
New syntax using x ← e to bind values on the left-hand-side of a function clause.
Instance search is more performant thanks to a new indexing structure.
Additionally, users can now control how instances should be selected
in the case multiple candidates exist.
User-facing options --exact-split, --keep-pattern-variables, and --postfix-projections
are now on by default.
Agda versioning scheme switches to the Haskell Package Versioning Policy
so Agda can be more reliably used as a library.
Major releases will now bump the second number in the version tuple: 2.7.0, 2.8.0, 2.9.0, ...
Agda supports GHC versions 8.6.5 to 9.10.1.
[Breaking] The option --overlapping-instances, which allows
backtracking during instance search, has been renamed to--backtracking-instance-search.
These options are now on by default:
--exact-split: Warn about clauses that are not definitional equalities.--keep-pattern-variables: Do not introduce dot patterns in interactive splitting.--postfix-projections: Print projections and projection patterns in postfix.--save-metas: Try to not unfold metavariable solutions in interface files.To revert to the old behavior, use options --no-....
The following options are now considered infective:
(Issue #5264)
--allow-exec--cumulativity--experimental-irrelevance--injective-type-constructors--omega-in-omega--rewriting--type-in-typeThis means that if a module has one of these flags enabled,
then all modules importing it must also have that flag enabled.
New warnings:
CoinductiveEtaRecord if a record is declared both coinductive and having eta-equality.
Used to be a hard error; now Agda continues, ignoring eta-equality.
ConflictingPragmaOptions if giving both --this and --that
when --this implies --no-that (and analogous for --no-this implies--that, etc).
ConstructorDoesNotFitInData when a constructor parameter
is too big (in the sense of universe level) for the target data type of the constructor.
Error warning, used to be a hard error.
DuplicateRecordDirectives if e.g. a record is declared both inductive and coinductive,
or declared inductive twice.
UselessMacro when a macro block does not contain any function definitions.
WarningProblem when trying to switch an unknown or non-benign warning with the -W option.
Used to be a hard error.
Rejected rewrite rules no longer cause a hard error but instead cause
an error warning. The following warnings were added to document the
various reasons for rejection:
RewriteLHSNotDefinitionOrConstructorRewriteVariablesNotBoundByLHSRewriteVariablesBoundMoreThanOnceRewriteLHSReducesRewriteHeadSymbolIsProjectionRewriteHeadSymbolIsProjectionLikeFunctionRewriteHeadSymbolIsTypeConstructorRewriteHeadSymbolContainsMetasRewriteConstructorParametersNotGeneralRewriteContainsUnsolvedMetaVariablesRewriteBlockedOnProblemsRewriteRequiresDefinitionsRewriteDoesNotTargetRewriteRelationRewriteBeforeFunctionDefinitionRewriteBeforeMutualFunctionDefinitionNew option --require-unique-meta-solutions
(turned on by default).
Disabling it with --no-require-unique-meta-solutions allows the type checker
to take advantage of INJECTIVE_FOR_INFERENCE pragmas (see below).
The --lossy-unification flag implies --no-require-unique-meta-solutions.
New pragma INJECTIVE_FOR_INFERENCE
which treats functions as injective for inferring implicit arguments if--no-require-unique-meta-solutions is given. The --no-require-unique-meta-solutions flag needs to be given in the
file where the function is used, and not necessarily in the file where it is defined.
For example:
postulate
reverse-≡ : {l l' : List A} → reverse l ≡ reverse l' → reverse l ≡ reverse l'
[]≡[] : [] ≡ []
[]≡[] = reverse-≡ (refl {x = reverse []})
does not work since Agda won't solve l and l' for [], even though it knows reverse l = reverse [].
If reverse is marked as injective with {-# INJECTIVE_FOR_INFERENCE reverse #-} this example will work.
Additions to the Agda syntax.
Left-hand side let:using x ← e
(PR #7078)
This new construct can be use in left-hand sides together with with andrewrite to give names to subexpressions. It is the left-hand side
counterpart of a let-binding and supports the same limited form of pattern
matching on eta-expandable record values.
It can be quite useful when you have a function doing a series of nestedwiths that share some expressions. Something like
fun : A → B fun x using z ← e with foo z ... | p with bar z ... | q = r
Here the expression e doesn't have to be repeated in the two with-expressions.
As in a with, multiple bindings can be separated by a |, and variables to
the left are in scope in bindings to the right.
Pattern synonyms can now expose existing instance arguments
(PR 7173).
Example:
data D : Set where
c : {{D}} → D
pattern p {{d}} = c {{d}}
This allows us to explicitly bind these argument in a pattern match
and supply them explicitly when using the pattern synonym in an expression.
f : D → D
f (p {{d = x}}) = p {{d = x}}
We cannot create new instance arguments this way, though.
The following is rejected:
data D : Set where
c : D → D
pattern p {{d}} = c dChanges to type checker and other components defining the Agda language.
Agda now uses discrimination trees to store and look up instance
definitions, rather than linearly searching through all instances for
a given "class" (PR #7109).
This is a purely internal change, and should not result in any change
to which programs are accepted or rejected. However, it significantly
improves the performance of instance search, especially for the case
of a "type class" indexed by a single type argument. The new lookup
procedure should never be slower than the previous implementation.
Changes to the meta-programming facilities.
[Breaking] Erased constructors are now supported in reflection machinery.
Quantity argument was added to data-cons. For erased constructors this
argument has a value of quantity-0, otherwise it's quantity-ω.defineData now requires setting quantity for each constructor.
Add new primitive to run instance search from reflection code:
-- Try to solve open instance constraints. When wrapped in `noConstraints`, -- fails if there are unsolved instance constraints left over that originate -- from the current macro invokation. Outside constraints are still attempted, -- but failure to solve them are ignored by `noConstraints`. solveInstanceConstraints : TC ⊤
A new reflection primitive workOnTypes : TC A → TC A was added toAgda.Builtin.Reflection. This runs the given computation at the type level,
which enables the use of erased things. In particular, this is needed when
working with (dependent) function types with erased arguments. For example,
one can get the type of the tuple constructor _,_ (which now takes its type
parameters as erased arguments, see above) and unify it with the current goal
as follows:
macro testM : Term → TC ⊤ testM hole = bindTC (getType (quote _,_)) (λ t → workOnTypes (unify hole t)) typeOfComma = testM
[Breaking] The Auto command
Agsy has been replaced by an entirely new implementation Mimer
(PR #6410).
This fixes problems where Auto would fail in the presence of language features
it did not know about, such as copatterns or anything cubical.
The reimplementation does not support case splitting (-c), disproving
(-d) or refining (-r).
The Agda input method for Emacs has been extended by several character bindings.
The list of changes can be obtained with a git diff on the sources:
git diff v2.6.4.3 v2.7.0 -- src/data/emacs-mode/agda-input.el
Highlighting some changes to Agda as a library.
New module Agda.Syntax.Common.KeywordRange providing type KwRange isomorphic to Range
to indicate source positions that just span keywords (PR #7162).
The motivation for KwRange is to distinguish such ranges from ranges for whole subtrees,
e.g. in data type Agda.Syntax.Concrete.Declaration.
API:
module Agda.Syntax.Common.KeywordRange where type KwRa...
This release fixes a regression in 2.6.4.3 and one in 2.6.4.
It aims to be API-compatible with 2.6.4.1 and 2.6.4.2.
Agda 2.6.4.3 supports GHC versions 8.6.5 to 9.8.1.
Closed issuesFor 2.6.4.3, the following issues were
closed
(see bug tracker):
withrewrite with instancesFull Changelog: v2.6.4.2...v2.6.4.3
RetroSearch is an open source project built by @garambo | Open a GitHub Issue
Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo
HTML:
3.2
| Encoding:
UTF-8
| Version:
0.7.4