From 9746e0774bea6758ec22529843798c67f342054c Mon Sep 17 00:00:00 2001 From: Eric Giovannini <ecg19@seas.upenn.edu> Date: Tue, 24 Oct 2023 02:57:01 +0100 Subject: [PATCH] Update SyntacticBisimilarity --- .../guarded-cubical/Syntax/SyntacticBisimilarity.agda | 2 ++ 1 file changed, 2 insertions(+) diff --git a/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda b/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda index b391130..37ad5d5 100644 --- a/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda +++ b/formalizations/guarded-cubical/Syntax/SyntacticBisimilarity.agda @@ -1,3 +1,4 @@ +{-# OPTIONS --allow-unsolved-metas #-} module Syntax.SyntacticBisimilarity where @@ -217,4 +218,5 @@ _≈->>_ M≈M' N≈N' = ≈-plugE (≈-bind N≈N') M≈M' ≈v-refl (isSetVal V Vâ‚ x y i iâ‚) = {!!} ≈v-refl (isPosetVal x xâ‚ i) = {!!} + -} -- GitLab