Library zoo_std.glist__code

Require Import zoo.prelude.
Require Import zoo.language.typeclasses.
Require Import zoo.language.notations.
Require Import zoo.options.

Notation "'glist٠Nil'" := (
  in_type "zoo_std.glist.t" 0
)(in custom zoo_tag
).
Notation "'glist٠Cons'" := (
  in_type "zoo_std.glist.t" 1
)(in custom zoo_tag
).

Definition glist٠rev_app : val :=
  𝗿𝗲𝗰 "rev_app" "t1" "t2" →
    𝗺𝗮𝘁𝗰𝗵 "t1" 𝘄𝗶𝘁𝗵
    | glist٠Nil →
        "t2"
    | glist٠Cons "v" "t1" →
        "rev_app" "t1" ‘glist٠Cons[ "v", "t2" ]
    𝗲𝗻𝗱.

Definition glist٠rev : val :=
  𝗳𝘂𝗻 "t" →
    glist٠rev_app "t" §glist٠Nil.