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

open scopes locally

Browse source
This commit is contained in:
Michael Sippel 2024-09-21 12:33:10 +02:00
parent 6f3b0fbc0b
commit 30fe571a39
Signed by: senvas
GPG key ID: F96CF119C34B64A6
2 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
coq/equiv_debruijn.v
View file

@ -1,7 +1,7 @@
Require Import terms_debruijn. Require Import terms_debruijn.
Open Scope ladder_type_scope. Local Open Scope ladder_type_scope.
Open Scope ladder_expr_scope. Local Open Scope ladder_expr_scope.
Create HintDb type_eq_hints. Create HintDb type_eq_hints.

2
coq/subtype_debruijn.v
View file

@ -18,6 +18,8 @@ Create HintDb subtype_hints.
Reserved Notation "s ':<=' t" (at level 50). Reserved Notation "s ':<=' t" (at level 50).
Reserved Notation "s '~<=' t" (at level 50). Reserved Notation "s '~<=' t" (at level 50).
Local Open Scope ladder_type_scope.
(* Representational Subtype *) (* Representational Subtype *)
Inductive is_repr_subtype : type_DeBruijn -> type_DeBruijn -> Prop := Inductive is_repr_subtype : type_DeBruijn -> type_DeBruijn -> Prop :=
| TSubRepr_Refl : forall t t', (t === t') -> (t :<= t') | TSubRepr_Refl : forall t t', (t === t') -> (t :<= t')