5

I installed Agda and started playing around. I tried to define an equality type and came up with the following solution:

data _≡_ {A : Set} : A -> A -> Set where
  refl : {x : A} -> x ≡ x

However, in Ulf Norell's and James Chapman's tutorial, they define it like this:

data _==_ {A : Set}(x : A) : A -> Set where
  refl : x == x

What's the difference (apart from the choice of a different character) to my version? Which one is recommended?

Turion
  • 5,684
  • 4
  • 26
  • 42
  • 1
    They generate different induction principles, the latter giving one that's easier to work with. Not sure you'd notice in Agda where you just use pattern matching anyways. The one you wrote is the original definition given by Martin-Lof but the other is the one used in Agda's standard lib. – daniel gratzer Aug 14 '15 at 17:53
  • 2
    [Related](http://stackoverflow.com/questions/8962873/parametrized-inductive-types-in-agda). But it seems like Agda became smarter and now turns indices into parameters, when possible. – effectfully Aug 14 '15 at 18:05

0 Answers0