syntaxAlchemist/ladder-calculus
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

paper: add appendix with coq listings

Browse source
This commit is contained in:
Michael Sippel 2024-08-07 15:59:03 +02:00
parent c7794d8a89
commit f135a5ed43
Signed by: senvas
GPG key ID: F96CF119C34B64A6
4 changed files with 58 additions and 5 deletions

6
coq/equiv.v
View file

@ -37,7 +37,7 @@ Include Terms.
Module Equiv.
(** Define all rewrite steps *)
(** Define all rewrite steps $\label{coq:type-dist}$ *)
Reserved Notation "S '-->distribute-ladder' T" (at level 40).
Inductive type_distribute_ladder : type_term -> type_term -> Prop :=
@ -111,7 +111,7 @@ Proof.
Qed.
(** Define the equivalence relation as reflexive, transitive hull. *)
(** Define the equivalence relation as reflexive, transitive hull. $\label{coq:type-equiv}$ *)
Reserved Notation " S '===' T " (at level 40).
Inductive type_eq : type_term -> type_term -> Prop :=
@ -163,7 +163,7 @@ Proof.
apply IHtype_eq1.
Qed.
(** "flat" types do not contain ladders *)
(** "flat" types do not contain ladders $\label{coq:type-flat}$ *)
Inductive type_is_flat : type_term -> Prop :=
| FlatUnit : (type_is_flat type_unit)
| FlatVar : forall x, (type_is_flat (type_var x))

3
coq/subst.v
View file

@ -4,8 +4,7 @@ Require Import terms.
Include Terms.
Module Subst.
(* scoped variable substitution in type terms *)
(* scoped variable substitution in type terms $\label{coq:subst-type}$ *)
Fixpoint type_subst (v:string) (n:type_term) (t0:type_term) :=
match t0 with
| type_var name => if (eqb v name) then n else t0