Commit e0300f5f authored by Jonas Kastberg's avatar Jonas Kastberg

Attempt at function from ktele to tele

parent 3724e8ef
From stdpp Require Import base tactics.
From stdpp Require Import base tactics telescopes.
From actris.logrel Require Import model.
Set Default Proof Using "Type".
......@@ -111,7 +111,14 @@ Proof.
rewrite IH. done.
Qed.
Fixpoint ktele_to_tele {Σ} (kt : ktele Σ) : tele :=
match kt with
| KTeleO => TeleO
| KTeleS b => TeleS (λ x, ktele_to_tele (b x))
end.
(*
(** We can define the identity function and composition of the [-t>] function *)
(* space. *)
Definition ktele_fun_id {Σ} {kt : ktele Σ} : kt -k> kt := ktele_bind id.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment