From a5b9cf152422239c58d8efee9db13775eb505f11 Mon Sep 17 00:00:00 2001 From: Andreas Stadelmeier Date: Mon, 18 Nov 2024 23:45:53 +0100 Subject: [PATCH] add Unfold' --- aspUnify.tex | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/aspUnify.tex b/aspUnify.tex index fef62c8..cc059c2 100644 --- a/aspUnify.tex +++ b/aspUnify.tex @@ -313,6 +313,12 @@ described in chapter \ref{sec:translation}. \type{T}_i \doteq \type{T}_i } \and +\inferrule[Unfold']{ + \tv{b} \lessdot \exptype{C}{\type{T}_1 \ldots \type{T}_n} +}{ + \type{T}_i \doteq \type{T}_i +} +\and \inferrule[Subst-Param]{ \type{T}' \doteq \type{S} \\ \type{T} \doteq \exptype{C}{\type{T}_1 \ldots, \type{T}', \ldots \type{T}_n} \\