I am wondering if there is anything in Agda that resembles Haskell's deriving Eq clause ---then I have an associated question below, as well.
For example, suppose I have types for a toy-language,
data Type : Set where
Nat : Type
Prp : Type
Then I can implement decidable equality by pattern matching and C-c C-a,
_≟ₜ_ : Decidable {A = Type} _≡_
Nat ≟ₜ Nat = yes refl
Nat ≟ₜ Prp = no (λ ())
Prp ≟ₜ Nat = no (λ ())
Prp ≟ₜ Prp = yes refl
I'm curious if this can be mechanised or automated somehow similar to the manner it is done in Haskell:
data Type = Nat | Prp deriving Eq
Thank-you!
While we're on the topic of types, I'd like to realise my formal types as Agda types: Nat is just natural numbers while Prp is small propositions.
⟦_⟧Type : Type → Set ?
⟦ Nat ⟧Type = ℕ
⟦ Prp ⟧Type = Set
Sadly this does not work. I tried to fix this with lifting but failed since I haven't a clue on how to use level lifting. Any help is appreciated!
An example usage of the above function would be,
record InterpretedFunctionSymbol : Set where
field
arity : ℕ
src tgt : Type
reify : Vec ⟦ src ⟧Type arity → ⟦ tgt ⟧Type
Thank-you for humouring me!