Neko.agda

module Neko where

data どうぶつ : Set where
    ねこ : どうぶつ
    その他 : どうぶつ 

data なきごえ : Set where
    にゃー : なきごえ
    あばば : なきごえ

data オカシイ : Set1 where

オカシイind : {なんとか : Set1} → オカシイ → なんとか
オカシイind ()

_ならば_ : Set1 → Set1 → Set1
ほげ ならば ぴよ = ほげ → ぴよ

infixr 40 _は_
infix 40 _は_じゃない
infixr 20 _ならば_
infix 50 _のなきごえ

data _は_ : {A : Set} → A → A → Set1 where
    同じ : {A : Set} → {ほげ : A} → ほげ は ほげ

_は_じゃない : {A : Set} → A → A → Set1
ほげ は ぴよ じゃない = ほげ は ぴよ ならば オカシイ

_のなきごえ : どうぶつ → なきごえ
ねこ のなきごえ = にゃー
その他 のなきごえ = あばば

postulate めんどくなった : オカシイ

真理 : {なんとか : どうぶつ} → なんとか は ねこ じゃない ならば なんとか のなきごえ は にゃー ならば オカシイ
真理 にょ = オカシイind めんどくなった