Skip to content

Instantly share code, notes, and snippets.

@Lysxia Lysxia/containers.v
Last active Sep 25, 2019

Embed
What would you like to do?
Set Implicit Arguments.
Set Contextual Implicit.
Record container : Type := {
shape : Type;
pos : shape -> Type;
}.
Inductive ext (c : container) (a : Type) : Type := {
this_shape : shape c;
this_rec : pos c this_shape -> a;
}.
Inductive list_shape a :=
| NilF : list_shape a
| ConsF : a -> list_shape a.
Definition list_pos a (s : list_shape a) : Type :=
match s with
| NilF => False (* no holes *)
| ConsF _ => True (* one hole x *)
end.
Definition list_container a : container := {|
shape := list_shape a;
pos := fun s => list_pos s;
|}.
Inductive Fix (c : container) : Type := MkFix (ext c (Fix c)).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.