-- 2012-02-22
module CorrectPrintingOfVariablesInSortCheckingForData where

data Bool : Set where
  true false : Bool

if_then_else_ : {A : Set2} → Bool → A → A → A
if true then a else b = a
if false then a else b = b

data foo : (y : Bool) → if y then Set else Set

data foo where
  bar : foo true

-- This should print
--   if y then Set else Set != Set of type Set₁
-- and not
--   if @0 then ...
