123456789101112131415161718192021222324252627282930313233343536373839 |
- -- 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
|