primStringEquality не уменьшается

Question

При запросе Агды нормализовать test в следующей программе:

data Bool : Set where
  T : Bool
  F : Bool
{-# BUILTIN BOOL  Bool  #-}
{-# BUILTIN TRUE  T #-}
{-# BUILTIN FALSE F #-}

postulate String : Set
postulate primStringEquality : String → String → Bool
{-# BUILTIN STRING String #-}

test : Bool
test = primStringEquality "bar" "foo"

Возвращает primStringEquality "bar" "foo" вместо F. Почему?

Answer 1

Это primitive для равенства вместо postulate. Мы также должны объявить BUILTIN STRING перед примитивами.

postulate String : Set
{-# BUILTIN STRING String #-}

primitive primStringEquality : String → String → Bool