Skip to content

Internal error for postulate in where block #443

@jespercockx

Description

@jespercockx

Minimal example:

open import Haskell.Prelude

test : ⊤
test = local
  where postulate local :{-# COMPILE AGDA2HS test #-}

Error message:

src/Agda2Hs/Compile/Function.hs:163:5-25: Non-exhaustive patterns in Function {..}

Should: compile the local definition as a postulate (i.e. a run-time error).

Metadata

Metadata

Assignees

Labels

bugSomething isn't working

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions