search

agda / agda2hs

Compiling Agda code to readable Haskell
https://agda.github.io/agda2hs
MIT License
178 stars 37 forks source link

Support `hiding` things from the prelude #356

Open omelkonian opened 2 months ago

omelkonian commented 2 months ago

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