Agda-2.3.2.2: test/succeed/DigitsInNames.agda

module DigitsInNames where

data 1D : Set where
  1d : 1D
  2d : 1D -> 1D