Skip to content

Instantly share code, notes, and snippets.

@pi8027

pi8027/rosetree.v

Last active September 5, 2022 19:10
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save pi8027/2d527aa06b6bcdd4045b911c79060876 to your computer and use it in GitHub Desktop.
Save pi8027/2d527aa06b6bcdd4045b911c79060876 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
rosetree.v
From mathcomp Require Import all_ssreflect.
Inductive tree := branch : seq tree -> tree.
Fixpoint size (t : tree) :=
let: branch ts := t in
(fix size_rec ts :=
if ts is t :: ts then
size t + size_rec ts
else 1) ts.
Fixpoint size' (t : tree) :=
let: branch ts := t in
foldl (fun n t => n + size' t) 1 ts.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment