Skip to content

Support hiding things from the prelude #356

@omelkonian

Description

@omelkonian

Currently the prelude namespace is imported in whole in the generated Haskell:

open import Haskell.Prelude hiding (const)

const : Nat  Nat  Nat
const n _ = n
{-# COMPILE AGDA2HS const #-}
import Numeric.Natural (Natural)

const :: Natural -> Natural -> Natural
const n _ = n

testConst :: Natural
testConst = const 42 0

It would be nice to instead enforce the visibility of the source Agda program:

import Numeric.Natural (Natural)
import Prelude hiding (const)

const :: Natural -> Natural -> Natural
const n _ = n

testConst :: Natural
testConst = const 42 0

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions