From 4bdd9e2780a94e6aa6cb98d8b790711ab77df3b1 Mon Sep 17 00:00:00 2001 From: jihgfee <jihgfee@gmail.com> Date: Fri, 1 May 2020 19:24:22 +0200 Subject: [PATCH] Attempt at function from ktele to tele --- theories/logrel/kind_tele.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/theories/logrel/kind_tele.v b/theories/logrel/kind_tele.v index 32af929..3e4d186 100644 --- a/theories/logrel/kind_tele.v +++ b/theories/logrel/kind_tele.v @@ -1,4 +1,4 @@ -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. -- GitLab