Skip to content

Instantly share code, notes, and snippets.

@Lysxia
Last active September 25, 2019 05:02
Show Gist options
  • Save Lysxia/21dd5fc7b79ced410b129f31ddf25c12 to your computer and use it in GitHub Desktop.
Save Lysxia/21dd5fc7b79ced410b129f31ddf25c12 to your computer and use it in GitHub Desktop.
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