Not Python

python.agda

data Python : Set where
  def_⦅_⦆⦂_ : {A B : Set} → A → B → Python → Python
  for_in̂_⦂_ : {A B : Set} → A → B → Python → Python
  if_⦂_ : Python → Python → Python
  if_⦂_else⦂_ : Python → Python → Python → Python 
  _≕_ : {A B : Set} → A → B → Python
  return_ : {A : Set} → A → Python

foo : {A B C D E : Set} → A → B → C → D → E → Python
foo a b c d e = def a ⦅ b ⦆⦂ 
                  for a in̂ b ⦂
                    if (c ≕ d) ⦂
                      return e
                    else⦂ 
                      return b