Skip to content

Internal error related to eta-expansion #78

@asr

Description

@asr
module Bug where

postulate
  D   : Set
  P   : D  Set
  k   : D
  Pk  : P k
  _≡_ : D  D  Set

c : (a : D)  P a  D
c a Pa = k
{-# ATP definition c #-}

postulate foo : c k Pk ≡ k
{-# ATP prove foo #-}
$ apia Bug.agda
An internal error has occurred. Please report this as a bug.
Location of the error: src/Apia/Utils/AgdaAPI/EtaExpansion.hs:74

Metadata

Metadata

Assignees

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions