agda/test/LaTeXAndHTML/succeed/Issue4580NegativeLiterals.agda

-- Andreas, 2020-04-12, issue #4580
-- Highlighting for builtins FROMNAT, FROMNEG, FROMSTRING

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

record Number (A : Set) : Set where
  field fromNat : Nat → A

record Negative (A : Set) : Set where
  field fromNeg : Nat → A

open Number {{...}} public
open Negative {{...}} public

{-# BUILTIN FROMNAT fromNat #-}  -- Should be highlighted.
{-# BUILTIN FROMNEG fromNeg #-}  -- Jump to definition should work.

instance
  NumberNat : Number Nat
  NumberNat = record { fromNat = λ n → n }

data Int : Set where
  pos : Nat → Int
  neg : Nat → Int

instance
  NumberInt : Number Int
  NumberInt = record { fromNat = pos }

  NegativeInt : Negative Int
  NegativeInt = record { fromNeg = λ { zero → pos 0 ; (suc n) → neg n } }

minusFive : Int
minusFive = -5

thm : -5 ≡ neg 4
thm = refl