Joshiryoku.agda

module Joshiryoku where

infix 1 >_< ^_^ ・_・
infix 2 （_） [_]
infix 3 o_o ∩_∩

data Mouse : Set where
    O : Mouse
    - : Mouse
    ω : Mouse

data Eyes : Set where
    >< : Eyes
    >_< : Mouse -> Eyes

    ^^ : Eyes
    ^_^ : Mouse -> Eyes

    ・・ : Eyes
    ・_・ : Mouse -> Eyes

data Rinkaku : Set where
    （_） : Eyes -> Rinkaku    
    [_] : Eyes -> Rinkaku

data Hand : Set where
    o_o : Rinkaku -> Hand

    ∩_∩ : Rinkaku -> Hand

hoge : Eyes
hoge = > O <

piyo : Rinkaku
piyo = [ ・ ω ・ ]

fuga : Hand
fuga = o （ ^ - ^ ） o