Agda 2

See the original README.md here.

This is a fork of agda/agda for personal use. The modifications are often implemented quickly and sloppily and is not properly tested. The code quality of the changes is subpar at best and in worst case does not work at all. No guarantees.

The branch "merged-hacks" is a merge of the different branches with the individual changes.

Branches

explicit-generalization

Allow the use of generalised variables with the explicit hiding.

variable A : Set
variable {B} : Set
variable ⦃ C ⦄ : Set
f : A → B → C → Set₁
f A {B} ⦃ C ⦄ _ _ _ = Set

• This breaking feature is hidden behind the flag: "--allow-explicit-generalizations" (recommended accompanying flag: "-WnoHiddenGeneralize").

• The difference is that normally, it is impossible to defined an explicit generalised variable. It transforms into an implicit/hidden.

Examples

module-oddities

Modifications to the module system to make it more uniform in its syntax.

• The breaking feature is hidden behind a flag: "--no-open-public-anonymous-modules". It changes anonymous modules written as module _ where to be non-open non-public by default. The old behaviour is now written open module _ public where or section where.

• Allow open and public for every module statement.

• New keyword section used as section where which is an opened anonymous public module (a synonym for open module _ public where.

Examples

non-name-instances

A hack to allow instances of more types.

instance _ : Set
instance _ : Set → Set

lookup : ∀{ℓ}{T : Set ℓ} → ⦃ T ⦄ → T
lookup ⦃ t ⦄ = t

set : Set
set = lookup

func : Set → Set
func = lookup

• Allow instance resolution of pi-types/function types. It behaves as if the function symbol is a name.

• Allow instance resolution of sorts (though not really that useful).

Examples 1 Examples 2

quantified-named-applications

Allow the use of scoped names in named applications.

variable {ℓ} : Level
variable {A} : Set ℓ
f : A → Level
f {A.ℓ = ℓ} _ = ℓ

record-module-hidings

Options for how a record module handls its parameters, besides the default hideOrKeepInstance.

Examples

inst-attr

An attribute alternative to the instance hiding on arguments. The following is working:

• The argument is added to the instance table (similar to instance arguments).

• If the argument is also implicit, and a value is not applied, then the meta will be resolved by instance resolution instead of unification (also similar to instance arguments).

infer : ∀{ℓ}{A : Set ℓ} → ⦃ A ⦄ → A
infer ⦃ x ⦄ = x

expl : @inst Set → Set
expl _ = infer

impl : @inst {Set} → Set
impl = infer

instance postulate set : Set

set' : Set
set' = impl

The attribute is also working with pattern synonyms, but something to note is that the instance argument check had to be disabled for this.

Command copy-paste collection for personal usage:

Update:

git checkout master
git pull
B=explicit-generalization       ; git checkout "$B" && git merge master
B=module-oddities               ; git checkout "$B" && git merge master
B=non-name-instances            ; git checkout "$B" && git merge master
B=quantified-named-applications ; git checkout "$B" && git merge master
B=record-module-hidings         ; git checkout "$B" && git merge master
B=inst-attr                     ; git checkout "$B" && git merge master
B=readme                        ; git checkout "$B" && git merge master

Pushing branches:

B=explicit-generalization       ; git checkout "$B" && git push
B=module-oddities               ; git checkout "$B" && git push
B=non-name-instances            ; git checkout "$B" && git push
B=quantified-named-applications ; git checkout "$B" && git push
B=record-module-hidings         ; git checkout "$B" && git push
B=inst-attr                     ; git checkout "$B" && git push
B=readme                        ; git checkout "$B" && git push

Merge to merged-hacks:

git checkout merged-hacks
git reset --hard master
B=explicit-generalization       ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=module-oddities               ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=non-name-instances            ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=quantified-named-applications ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=record-module-hidings         ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=inst-attr                     ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"
B=readme                        ; git merge "$B" --squash && git commit -m "Squashed commit of branch: $B"