Skip to content

Commit 13082a0

Browse files
effectfullyramsay-t
effectfully
and
ramsay-t
authored
Add 'VerifiedCompilation' blob (#6380)
* Add 'VerifiedCompilation' blob * Comments and tests removed to make a clean PR. This can be reverted in a later branch. --------- Co-authored-by: Ramsay Taylor <[email protected]>
1 parent 1996152 commit 13082a0

File tree

8 files changed

+1015
-0
lines changed

8 files changed

+1015
-0
lines changed

‎plutus-metatheory/changelog.d/20240502_122129_ramsay.taylor_verified_compilation.rst‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
# Added
2+
3+
Initial Translation Relation for the Untyped Case of Case simplification phase

‎plutus-metatheory/src/Untyped.lagda.md‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -40,6 +40,12 @@ open Untyped
4040

4141
## Well-scoped Syntax
4242

43+
This defines the syntax for UPLC and requires that it be "well scoped", which
44+
is that only variables in the context are used. The context uses de Bruijn naming,
45+
so the variables are numbered. This numbering is provided by an inductively defined
46+
natural number, which uses the Maybe type (so: `Nothing` = zero, `Just Just Nothing` = 2)
47+
to allow direct translation to Haskell.
48+
4349
```
4450
data _⊢ (X : Set) : Set where
4551
` : X → X ⊢

‎plutus-metatheory/src/Utils.lagda.md‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -175,6 +175,10 @@ postulate ByteString : Set
175175
{-# FOREIGN GHC import qualified Data.ByteString as BS #-}
176176
{-# COMPILE GHC ByteString = type BS.ByteString #-}
177177
178+
postulate
179+
eqByteString : ByteString → ByteString → Bool
180+
{-# COMPILE GHC eqByteString = (==) #-}
181+
178182
```
179183
## Record Types
180184
```
@@ -246,13 +250,25 @@ postulate Bls12-381-G1-Element : Set
246250
{-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G1 as G1 #-}
247251
{-# COMPILE GHC Bls12-381-G1-Element = type G1.Element #-}
248252
253+
postulate
254+
eqBls12-381-G1-Element : Bls12-381-G1-Element → Bls12-381-G1-Element → Bool
255+
{-# COMPILE GHC eqBls12-381-G1-Element = (==) #-}
256+
249257
postulate Bls12-381-G2-Element : Set
250258
{-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.G2 as G2 #-}
251259
{-# COMPILE GHC Bls12-381-G2-Element = type G2.Element #-}
252260
261+
postulate
262+
eqBls12-381-G2-Element : Bls12-381-G2-Element → Bls12-381-G2-Element → Bool
263+
{-# COMPILE GHC eqBls12-381-G2-Element = (==) #-}
264+
253265
postulate Bls12-381-MlResult : Set
254266
{-# FOREIGN GHC import qualified PlutusCore.Crypto.BLS12_381.Pairing as Pairing #-}
255267
{-# COMPILE GHC Bls12-381-MlResult = type Pairing.MlResult #-}
268+
269+
postulate
270+
eqBls12-381-MlResult : Bls12-381-MlResult → Bls12-381-MlResult → Bool
271+
{-# COMPILE GHC eqBls12-381-MlResult = (==) #-}
256272
```
257273

258274
## Kinds

‎plutus-metatheory/src/VerifiedCompilation/Equality.lagda.md‎

Lines changed: 334 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,334 @@
1+
---
2+
title: VerifiedCompilation.Equality
3+
layout: page
4+
---
5+
# Verified Compilation Equality
6+
```
7+
module VerifiedCompilation.Equality where
8+
```
9+
10+
## Decidable Equivalence
11+
12+
There are various points in the Translation definitions where we need to compare terms
13+
for equality. It is almost always the case that an unchanged term is a valid translation; in
14+
many of the translations there are parts that must remain untouched.
15+
16+
```
17+
import Relation.Binary.PropositionalEquality as Eq
18+
open Eq using (_≡_; refl; isEquivalence; cong)
19+
open import Data.Nat using (ℕ)
20+
open import Data.Empty using (⊥)
21+
open import RawU using (TmCon; tmCon; decTag; TyTag; ⟦_⟧tag; decTagCon; tmCon2TagCon)
22+
open import Relation.Binary.Definitions using (DecidableEquality)
23+
open import Builtin.Constant.AtomicType using (AtomicTyCon; decAtomicTyCon; ⟦_⟧at)
24+
open import Agda.Builtin.Bool using (true; false)
25+
open import Data.List using (List; []; _∷_)
26+
open import Data.List.Relation.Binary.Pointwise.Base using (Pointwise)
27+
open import Data.List.Relation.Binary.Pointwise using (Pointwise-≡⇒≡; ≡⇒Pointwise-≡)
28+
open import Data.List.Properties using (≡-dec)
29+
open import Relation.Binary.Core using (REL)
30+
open import Level using (Level)
31+
open import Builtin using (Builtin; decBuiltin)
32+
open import Builtin.Signature using (_⊢♯)
33+
import Data.Nat.Properties using (_≟_)
34+
open import Data.Integer using (ℤ)
35+
import Data.Integer.Properties using (_≟_)
36+
import Data.String.Properties using (_≟_)
37+
import Data.Bool.Properties using (_≟_)
38+
import Data.Unit.Properties using (_≟_)
39+
open import Untyped using (_⊢; `; ƛ; case; constr; _·_; force; delay; con; builtin; error)
40+
import Relation.Unary as Unary using (Decidable)
41+
import Relation.Binary.Definitions as Binary using (Decidable)
42+
open import Relation.Nullary using (Dec; yes; no; ¬_)
43+
open import Data.Product using (_,_)
44+
open import Relation.Nullary.Product using (_×-dec_)
45+
open import Utils as U using (Maybe; nothing; just; Either)
46+
import Data.List.Properties as LP using (≡-dec)
47+
open import Builtin.Constant.AtomicType using (decAtomicTyCon)
48+
open import Agda.Builtin.TrustMe using (primTrustMe)
49+
open import Agda.Builtin.String using (String; primStringEquality)
50+
```
51+
Instances of `DecEq` will provide a Decidable Equality procedure for their type.
52+
53+
```
54+
record DecEq (A : Set) : Set where
55+
field _≟_ : DecidableEquality A
56+
open DecEq {{...}} public
57+
```
58+
Several of the decision procedures depend on other `DecEq` instances, so it is useful
59+
to give them types and bind them to instance declarations first and then use them in the
60+
implementations further down.
61+
62+
```
63+
decEq-TmCon : DecidableEquality TmCon
64+
65+
decEq-TyTag : DecidableEquality TyTag
66+
67+
decEq-⟦_⟧tag : ( t : TyTag ) → DecidableEquality ⟦ t ⟧tag
68+
```
69+
# Pointwise Decisions
70+
71+
We often need to show that one list of AST elements is a valid translation
72+
of another list of AST elements by showing the `n`th element of one is a translation of the
73+
`n`th element of the other, pointwise.
74+
75+
```
76+
decPointwise : {l₁ l₂ : Level} { A B : Set l₁ } { _~_ : A → B → Set l₂} → Binary.Decidable _~_ → Binary.Decidable (Pointwise _~_)
77+
decPointwise dec [] [] = yes Pointwise.[]
78+
decPointwise dec [] (x ∷ ys) = no (λ ())
79+
decPointwise dec (x ∷ xs) [] = no (λ ())
80+
decPointwise dec (x ∷ xs) (y ∷ ys) with dec x y | decPointwise dec xs ys
81+
... | yes p | yes q = yes (p Pointwise.∷ q)
82+
... | yes _ | no ¬q = no λ where (_ Pointwise.∷ xs~ys) → ¬q xs~ys
83+
... | no ¬p | _ = no λ where (x∼y Pointwise.∷ _) → ¬p x∼y
84+
```
85+
86+
## Decidable Equality Instances
87+
88+
Creating Instance declarations for various Decidable Equality functions to be used
89+
when creating translation decision procedures.
90+
91+
```
92+
decEq-⊢ : ∀{X} {{_ : DecEq X}} → DecidableEquality (X ⊢)
93+
94+
instance
95+
DecEq-Maybe : ∀{A} {{_ : DecEq A}} → DecEq (Maybe A)
96+
DecEq-Maybe ._≟_ = M.≡-dec _≟_
97+
where import Data.Maybe.Properties as M
98+
99+
EmptyEq : DecEq ⊥
100+
EmptyEq = record { _≟_ = λ () }
101+
102+
DecAtomicTyCon : DecEq AtomicTyCon
103+
DecAtomicTyCon ._≟_ = decAtomicTyCon
104+
105+
DecEq-TmCon : DecEq TmCon
106+
DecEq-TmCon ._≟_ = decEq-TmCon
107+
108+
DecEq-⊢ : ∀{X} {{_ : DecEq X}} → DecEq (X ⊢)
109+
DecEq-⊢ ._≟_ = decEq-⊢
110+
111+
DecEq-List-⊢ : ∀{X} {{_ : DecEq X}} → DecEq (List (X ⊢))
112+
DecEq-List-⊢ ._≟_ = LP.≡-dec decEq-⊢
113+
114+
DecEq-Builtin : DecEq Builtin
115+
DecEq-Builtin ._≟_ = decBuiltin
116+
117+
DecEq-ℕ : DecEq ℕ
118+
DecEq-ℕ ._≟_ = Data.Nat.Properties._≟_
119+
120+
DecEq-ℤ : DecEq ℤ
121+
DecEq-ℤ ._≟_ = Data.Integer.Properties._≟_
122+
123+
DecEq-TyTag : DecEq TyTag
124+
DecEq-TyTag ._≟_ = decEq-TyTag
125+
126+
```
127+
The `TmCon` type inserts constants into Terms, so it is built from the
128+
type tag and semantics equality decision procedures.
129+
130+
Type Tags (`TyTag`) are just a list of constructors to represent each
131+
of the builtin types, or they are a structure built on top of those using
132+
`list` or `pair`.
133+
```
134+
decEq-TyTag (_⊢♯.atomic x) (_⊢♯.atomic x₁) with (decAtomicTyCon x x₁)
135+
... | yes refl = yes refl
136+
... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl }
137+
decEq-TyTag (_⊢♯.atomic x) (_⊢♯.list t') = no (λ ())
138+
decEq-TyTag (_⊢♯.atomic x) (_⊢♯.pair t' t'') = no (λ ())
139+
decEq-TyTag (_⊢♯.list t) (_⊢♯.atomic x) = no (λ ())
140+
decEq-TyTag (_⊢♯.list t) (_⊢♯.list t') with t ≟ t'
141+
... | yes refl = yes refl
142+
... | no ¬p = no λ { refl → ¬p refl }
143+
decEq-TyTag (_⊢♯.list t) (_⊢♯.pair t' t'') = no (λ ())
144+
decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.atomic x) = no (λ ())
145+
decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.list t') = no (λ ())
146+
decEq-TyTag (_⊢♯.pair t t₁) (_⊢♯.pair t' t'') with (t ≟ t') ×-dec (t₁ ≟ t'')
147+
... | yes (refl , refl) = yes refl
148+
... | no ¬pq = no λ { refl → ¬pq (refl , refl) }
149+
150+
```
151+
The equality of the semantics of constants will depend on the equality of
152+
the underlying types, so this can leverage the standard library decision
153+
procedures.
154+
155+
```
156+
record HsEq (A : Set) : Set where
157+
field
158+
hsEq : A → A → Agda.Builtin.Bool.Bool
159+
160+
open HsEq {{...}} public
161+
162+
postulate
163+
magicNeg : ∀ {A : Set} {a b : A} → ¬ a ≡ b
164+
165+
magicBoolDec : {A : Set} → {a b : A} → Agda.Builtin.Bool.Bool → Dec (a ≡ b)
166+
magicBoolDec true = yes primTrustMe
167+
magicBoolDec false = no magicNeg
168+
169+
builtinEq : {A : Set} {{_ : HsEq A}} → Binary.Decidable {A = A} _≡_
170+
builtinEq x y = magicBoolDec (hsEq x y)
171+
172+
instance
173+
HsEqBytestring : HsEq U.ByteString
174+
HsEqBytestring = record { hsEq = U.eqByteString }
175+
HsEqBlsG1 : HsEq U.Bls12-381-G1-Element
176+
HsEqBlsG1 = record { hsEq = U.eqBls12-381-G1-Element }
177+
HsEqBlsG2 : HsEq U.Bls12-381-G2-Element
178+
HsEqBlsG2 = record { hsEq = U.eqBls12-381-G2-Element }
179+
HsEqBlsMlResult : HsEq U.Bls12-381-MlResult
180+
HsEqBlsMlResult = record { hsEq = U.eqBls12-381-MlResult }
181+
182+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aInteger ⟧tag = Data.Integer.Properties._≟_
183+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aBytestring ⟧tag = builtinEq
184+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aString ⟧tag = Data.String.Properties._≟_
185+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aUnit ⟧tag = Data.Unit.Properties._≟_
186+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aBool ⟧tag = Data.Bool.Properties._≟_
187+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aData ⟧tag v v₁ = magicBoolDec (U.eqDATA v v₁)
188+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g1-element ⟧tag = builtinEq
189+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-g2-element ⟧tag = builtinEq
190+
decEq-⟦ _⊢♯.atomic AtomicTyCon.aBls12-381-mlresult ⟧tag = builtinEq
191+
decEq-⟦ _⊢♯.list t ⟧tag U.[] U.[] = yes refl
192+
decEq-⟦ _⊢♯.list t ⟧tag U.[] (x U.∷ v₁) = no λ ()
193+
decEq-⟦ _⊢♯.list t ⟧tag (x U.∷ v) U.[] = no (λ ())
194+
decEq-⟦ _⊢♯.list t ⟧tag (x U.∷ v) (x₁ U.∷ v₁) with decEq-⟦ t ⟧tag x x₁
195+
... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl }
196+
... | yes refl with decEq-⟦ _⊢♯.list t ⟧tag v v₁
197+
... | yes refl = yes refl
198+
... | no ¬v=v₁ = no λ { refl → ¬v=v₁ refl }
199+
decEq-⟦ _⊢♯.pair t t₁ ⟧tag (proj₁ U., proj₂) (proj₃ U., proj₄) with (decEq-⟦ t ⟧tag proj₁ proj₃) ×-dec (decEq-⟦ t₁ ⟧tag proj₂ proj₄)
200+
... | yes ( refl , refl ) = yes refl
201+
... | no ¬pq = no λ { refl → ¬pq (refl , refl) }
202+
decEq-TmCon (tmCon t x) (tmCon t₁ x₁) with t ≟ t₁
203+
... | no ¬t=t₁ = no λ { refl → ¬t=t₁ refl }
204+
... | yes refl with decEq-⟦ t ⟧tag x x₁
205+
... | yes refl = yes refl
206+
... | no ¬x=x₁ = no λ { refl → ¬x=x₁ refl }
207+
208+
```
209+
The Decidable Equality of terms needs to use the other instances, so we can present
210+
that now.
211+
```
212+
-- This terminating declaration shouldn't be needed?
213+
-- It is the mutual recursion with list equality that requires it.
214+
{-# TERMINATING #-}
215+
decEq-⊢ (` x) (` x₁) with x ≟ x₁
216+
... | yes refl = yes refl
217+
... | no ¬p = no λ { refl → ¬p refl }
218+
decEq-⊢ (` x) (ƛ t₁) = no (λ ())
219+
decEq-⊢ (` x) (t₁ · t₂) = no (λ ())
220+
decEq-⊢ (` x) (force t₁) = no (λ ())
221+
decEq-⊢ (` x) (delay t₁) = no (λ ())
222+
decEq-⊢ (` x) (con x₁) = no (λ ())
223+
decEq-⊢ (` x) (constr i xs) = no (λ ())
224+
decEq-⊢ (` x) (case t₁ ts) = no (λ ())
225+
decEq-⊢ (` x) (builtin b) = no (λ ())
226+
decEq-⊢ (` x) error = no (λ ())
227+
decEq-⊢ (ƛ t) (` x) = no (λ ())
228+
decEq-⊢ (ƛ t) (ƛ t₁) with t ≟ t₁
229+
... | yes p = yes (cong ƛ p)
230+
... | no ¬p = no λ { refl → ¬p refl }
231+
decEq-⊢ (ƛ t) (t₁ · t₂) = no (λ ())
232+
decEq-⊢ (ƛ t) (force t₁) = no (λ ())
233+
decEq-⊢ (ƛ t) (delay t₁) = no (λ ())
234+
decEq-⊢ (ƛ t) (con x) = no (λ ())
235+
decEq-⊢ (ƛ t) (constr i xs) = no (λ ())
236+
decEq-⊢ (ƛ t) (case t₁ ts) = no (λ ())
237+
decEq-⊢ (ƛ t) (builtin b) = no (λ ())
238+
decEq-⊢ (ƛ t) error = no (λ ())
239+
decEq-⊢ (t · t₂) (` x) = no (λ ())
240+
decEq-⊢ (t · t₂) (ƛ t₁) = no (λ ())
241+
decEq-⊢ (t · t₂) (t₁ · t₃) with (t ≟ t₁) ×-dec (t₂ ≟ t₃)
242+
... | yes ( refl , refl ) = yes refl
243+
... | no ¬p = no λ { refl → ¬p (refl , refl) }
244+
decEq-⊢ (t · t₂) (force t₁) = no (λ ())
245+
decEq-⊢ (t · t₂) (delay t₁) = no (λ ())
246+
decEq-⊢ (t · t₂) (con x) = no (λ ())
247+
decEq-⊢ (t · t₂) (constr i xs) = no (λ ())
248+
decEq-⊢ (t · t₂) (case t₁ ts) = no (λ ())
249+
decEq-⊢ (t · t₂) (builtin b) = no (λ ())
250+
decEq-⊢ (t · t₂) error = no (λ ())
251+
decEq-⊢ (force t) (` x) = no (λ ())
252+
decEq-⊢ (force t) (ƛ t₁) = no (λ ())
253+
decEq-⊢ (force t) (t₁ · t₂) = no (λ ())
254+
decEq-⊢ (force t) (force t₁) with t ≟ t₁
255+
... | yes refl = yes refl
256+
... | no ¬p = no λ { refl → ¬p refl }
257+
decEq-⊢ (force t) (delay t₁) = no (λ ())
258+
decEq-⊢ (force t) (con x) = no (λ ())
259+
decEq-⊢ (force t) (constr i xs) = no (λ ())
260+
decEq-⊢ (force t) (case t₁ ts) = no (λ ())
261+
decEq-⊢ (force t) (builtin b) = no (λ ())
262+
decEq-⊢ (force t) error = no (λ ())
263+
decEq-⊢ (delay t) (` x) = no (λ ())
264+
decEq-⊢ (delay t) (ƛ t₁) = no (λ ())
265+
decEq-⊢ (delay t) (t₁ · t₂) = no (λ ())
266+
decEq-⊢ (delay t) (force t₁) = no (λ ())
267+
decEq-⊢ (delay t) (delay t₁) with t ≟ t₁
268+
... | yes refl = yes refl
269+
... | no ¬p = no λ { refl → ¬p refl }
270+
decEq-⊢ (delay t) (con x) = no (λ ())
271+
decEq-⊢ (delay t) (constr i xs) = no (λ ())
272+
decEq-⊢ (delay t) (case t₁ ts) = no (λ ())
273+
decEq-⊢ (delay t) (builtin b) = no (λ ())
274+
decEq-⊢ (delay t) error = no (λ ())
275+
decEq-⊢ (con x) (` x₁) = no (λ ())
276+
decEq-⊢ (con x) (ƛ t₁) = no (λ ())
277+
decEq-⊢ (con x) (t₁ · t₂) = no (λ ())
278+
decEq-⊢ (con x) (force t₁) = no (λ ())
279+
decEq-⊢ (con x) (delay t₁) = no (λ ())
280+
decEq-⊢ (con x) (con x₁) with x ≟ x₁
281+
... | yes refl = yes refl
282+
... | no ¬p = no λ { refl → ¬p refl }
283+
decEq-⊢ (con x) (constr i xs) = no (λ ())
284+
decEq-⊢ (con x) (case t₁ ts) = no (λ ())
285+
decEq-⊢ (con x) (builtin b) = no (λ ())
286+
decEq-⊢ (con x) error = no (λ ())
287+
decEq-⊢ (constr i xs) (` x) = no (λ ())
288+
decEq-⊢ (constr i xs) (ƛ t₁) = no (λ ())
289+
decEq-⊢ (constr i xs) (t₁ · t₂) = no (λ ())
290+
decEq-⊢ (constr i xs) (force t₁) = no (λ ())
291+
decEq-⊢ (constr i xs) (delay t₁) = no (λ ())
292+
decEq-⊢ (constr i xs) (con x) = no (λ ())
293+
decEq-⊢ (constr i xs) (constr i₁ xs₁) with (i ≟ i₁) ×-dec (xs ≟ xs₁)
294+
... | yes (refl , refl) = yes refl
295+
... | no ¬pq = no λ { refl → ¬pq (refl , refl) }
296+
decEq-⊢ (constr i xs) (case t₁ ts) = no (λ ())
297+
decEq-⊢ (constr i xs) (builtin b) = no (λ ())
298+
decEq-⊢ (constr i xs) error = no (λ ())
299+
decEq-⊢ (case t ts) (` x) = no (λ ())
300+
decEq-⊢ (case t ts) (ƛ t₁) = no (λ ())
301+
decEq-⊢ (case t ts) (t₁ · t₂) = no (λ ())
302+
decEq-⊢ (case t ts) (force t₁) = no (λ ())
303+
decEq-⊢ (case t ts) (delay t₁) = no (λ ())
304+
decEq-⊢ (case t ts) (con x) = no (λ ())
305+
decEq-⊢ (case t ts) (constr i xs) = no (λ ())
306+
decEq-⊢ (case t ts) (case t₁ ts₁) with (decEq-⊢ t t₁) ×-dec (ts ≟ ts₁)
307+
... | yes (refl , refl) = yes refl
308+
... | no ¬pq = no λ { refl → ¬pq (refl , refl) }
309+
decEq-⊢ (case t ts) (builtin b) = no (λ ())
310+
decEq-⊢ (case t ts) error = no (λ ())
311+
decEq-⊢ (builtin b) (` x) = no (λ ())
312+
decEq-⊢ (builtin b) (ƛ t₁) = no (λ ())
313+
decEq-⊢ (builtin b) (t₁ · t₂) = no (λ ())
314+
decEq-⊢ (builtin b) (force t₁) = no (λ ())
315+
decEq-⊢ (builtin b) (delay t₁) = no (λ ())
316+
decEq-⊢ (builtin b) (con x) = no (λ ())
317+
decEq-⊢ (builtin b) (constr i xs) = no (λ ())
318+
decEq-⊢ (builtin b) (case t₁ ts) = no (λ ())
319+
decEq-⊢ (builtin b) (builtin b₁) with b ≟ b₁
320+
... | yes refl = yes refl
321+
... | no ¬p = no λ { refl → ¬p refl }
322+
decEq-⊢ (builtin b) error = no (λ ())
323+
decEq-⊢ error (` x) = no (λ ())
324+
decEq-⊢ error (ƛ t₁) = no (λ ())
325+
decEq-⊢ error (t₁ · t₂) = no (λ ())
326+
decEq-⊢ error (force t₁) = no (λ ())
327+
decEq-⊢ error (delay t₁) = no (λ ())
328+
decEq-⊢ error (con x) = no (λ ())
329+
decEq-⊢ error (constr i xs) = no (λ ())
330+
decEq-⊢ error (case t₁ ts) = no (λ ())
331+
decEq-⊢ error (builtin b) = no (λ ())
332+
decEq-⊢ error error = yes refl
333+
334+
```

0 commit comments

Comments
 (0)