misc metatheory cleanup (#4164)

* remove arity from Scoped syntax files as there is not scoped semantics anymore
* misc renaming of stuff

plutus-metatheory/src/Algorithmic.lagda

@@ -91,85 +91,85 @@ A term is indexed over by its context and type.  A term is a variable,
 an abstraction, an application, a type abstraction, or a type
 application.
 \begin{code}
-ISIG : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢Nf⋆ *
-ISIG ifThenElse = _ ,, ∅ ,⋆ * , con bool , ne (` Z) , ne (` Z) ,, ne (` Z)
-ISIG addInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG subtractInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG multiplyInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG divideInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG quotientInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG remainderInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG modInteger = ∅ ,, ∅ , con integer , con integer ,, con integer
-ISIG lessThanInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG lessThanEqualsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG equalsInteger = ∅ ,, ∅ , con integer , con integer ,, con bool
-ISIG appendByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bytestring
-ISIG lessThanByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG lessThanEqualsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG sha2-256 = ∅ ,, ∅ , con bytestring ,, con bytestring
-ISIG sha3-256 = ∅ ,, ∅ , con bytestring ,, con bytestring
-ISIG verifySignature = ∅ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool
-ISIG equalsByteString = ∅ ,, ∅ , con bytestring , con bytestring ,, con bool
-ISIG appendString = ∅ ,, ∅ , con string , con string ,, con string
-ISIG trace = _ ,, ∅ ,⋆ * , con string , ne (` Z) ,, ne (` Z)
-ISIG equalsString = ∅ ,, ∅ , con string , con string ,, con bool
-ISIG encodeUtf8 = ∅ ,, ∅ , con string ,, con bytestring
-ISIG decodeUtf8 = ∅ ,, ∅ , con bytestring ,, con string
-ISIG fstPair =
+sig : Builtin → Σ Ctx⋆ λ Φ → Ctx Φ × Φ ⊢Nf⋆ *
+sig ifThenElse = _ ,, ∅ ,⋆ * , con bool , ne (` Z) , ne (` Z) ,, ne (` Z)
+sig addInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig subtractInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig multiplyInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig divideInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig quotientInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig remainderInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig modInteger = _ ,, ∅ , con integer , con integer ,, con integer
+sig lessThanInteger = _ ,, ∅ , con integer , con integer ,, con bool
+sig lessThanEqualsInteger = _ ,, ∅ , con integer , con integer ,, con bool
+sig equalsInteger = _ ,, ∅ , con integer , con integer ,, con bool
+sig appendByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bytestring
+sig lessThanByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+sig lessThanEqualsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+sig sha2-256 = _ ,, ∅ , con bytestring ,, con bytestring
+sig sha3-256 = _ ,, ∅ , con bytestring ,, con bytestring
+sig verifySignature = _ ,, ∅ , con bytestring , con bytestring , con bytestring ,, con bool
+sig equalsByteString = _ ,, ∅ , con bytestring , con bytestring ,, con bool
+sig appendString = _ ,, ∅ , con string , con string ,, con string
+sig trace = _ ,, ∅ ,⋆ * , con string , ne (` Z) ,, ne (` Z)
+sig equalsString = _ ,, ∅ , con string , con string ,, con bool
+sig encodeUtf8 = _ ,, ∅ , con string ,, con bytestring
+sig decodeUtf8 = _ ,, ∅ , con bytestring ,, con string
+sig fstPair =
   _ ,, ∅ ,⋆ * ,⋆ * , con (pair (ne (` (S Z))) (ne (` Z))) ,, ne (` (S Z))
-ISIG sndPair = 
+sig sndPair = 
   _ ,, ∅ ,⋆ * ,⋆ * , con (pair (ne (` (S Z))) (ne (` Z))) ,, ne (` Z)
-ISIG nullList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con bool
-ISIG headList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, ne (` Z)
-ISIG tailList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con (list (ne (` Z)))
-ISIG chooseList =
+sig nullList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con bool
+sig headList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, ne (` Z)
+sig tailList = _ ,, ∅ ,⋆ * , con (list (ne (` Z))) ,, con (list (ne (` Z)))
+sig chooseList =
   _
   ,,
   ∅ ,⋆ * ,⋆ * , ne (` (S Z)) , ne (` (S Z)) , con (list (ne (` Z)))
   ,,
   ne (` (S Z)) 
-ISIG constrData = _ ,, ∅ , con integer , con (list (con Data)) ,, con Data
-ISIG mapData = _ ,, ∅ , con (pair (con Data) (con Data)) ,, con Data
-ISIG listData = _ ,, ∅ , con (list (con Data)) ,, con Data
-ISIG iData = _ ,, ∅ , con integer ,, con Data
-ISIG bData = _ ,, ∅ , con bytestring ,, con Data
-ISIG unConstrData =
+sig constrData = _ ,, ∅ , con integer , con (list (con Data)) ,, con Data
+sig mapData = _ ,, ∅ , con (pair (con Data) (con Data)) ,, con Data
+sig listData = _ ,, ∅ , con (list (con Data)) ,, con Data
+sig iData = _ ,, ∅ , con integer ,, con Data
+sig bData = _ ,, ∅ , con bytestring ,, con Data
+sig unConstrData =
   _ ,, ∅ , con Data ,, con (pair (con integer) (con (list (con Data))))
-ISIG unMapData = _ ,, ∅ , con Data ,, con (pair (con Data) (con Data))
-ISIG unListData = _ ,, ∅ , con Data ,, con (list (con Data))
-ISIG unIData = _ ,, ∅ , con Data ,, con integer
-ISIG unBData = _ ,, ∅ , con Data ,, con bytestring
-ISIG equalsData = _ ,, ∅ , con Data , con Data ,, con bool
-ISIG chooseData =
+sig unMapData = _ ,, ∅ , con Data ,, con (pair (con Data) (con Data))
+sig unListData = _ ,, ∅ , con Data ,, con (list (con Data))
+sig unIData = _ ,, ∅ , con Data ,, con integer
+sig unBData = _ ,, ∅ , con Data ,, con bytestring
+sig equalsData = _ ,, ∅ , con Data , con Data ,, con bool
+sig chooseData =
   _
   ,,
   ∅ ,⋆ * , ne (` Z) , ne (` Z) , ne (` Z) , ne (` Z) , ne (` Z) , con Data
   ,,
   ne (` Z)
-ISIG chooseUnit = _ ,, ∅ ,⋆ * , ne (` Z) , con unit ,, ne (` Z)
-ISIG mkPairData =
+sig chooseUnit = _ ,, ∅ ,⋆ * , ne (` Z) , con unit ,, ne (` Z)
+sig mkPairData =
   _ ,, ∅ , con Data , con Data ,, con (pair (con Data) (con Data)) 
-ISIG mkNilData = _ ,, ∅ , con unit ,, con (list (con Data))
-ISIG mkNilPairData = _ ,, ∅ , con unit ,, con (list (con (pair (con Data) (con Data))))
-ISIG mkCons =
+sig mkNilData = _ ,, ∅ , con unit ,, con (list (con Data))
+sig mkNilPairData = _ ,, ∅ , con unit ,, con (list (con (pair (con Data) (con Data))))
+sig mkCons =
   _ ,, ∅ , con Data , con (list (con Data)) ,, con (list (con Data))
-ISIG consByteString = _ ,, ∅ , con integer , con bytestring ,, con bytestring
-ISIG sliceByteString =
+sig consByteString = _ ,, ∅ , con integer , con bytestring ,, con bytestring
+sig sliceByteString =
   _ ,, ∅ , con integer , con integer , con bytestring ,, con bytestring
-ISIG lengthOfByteString = _ ,, ∅ , con bytestring ,, con integer
-ISIG indexByteString = _ ,, ∅ , con bytestring , con integer ,, con integer
-ISIG blake2b-256 = _ ,, ∅ , con bytestring ,, con bytestring
+sig lengthOfByteString = _ ,, ∅ , con bytestring ,, con integer
+sig indexByteString = _ ,, ∅ , con bytestring , con integer ,, con integer
+sig blake2b-256 = _ ,, ∅ , con bytestring ,, con bytestring
 
-isig2type : (Φ : Ctx⋆) → Ctx Φ → Φ ⊢Nf⋆ * → ∅ ⊢Nf⋆ *
-isig2type .∅ ∅ C = C
-isig2type (Φ ,⋆ J) (Γ ,⋆ J) C = isig2type Φ Γ (Π C)
-isig2type Φ        (Γ ,  A) C = isig2type Φ Γ (A ⇒ C)
+sig2type : (Φ : Ctx⋆) → Ctx Φ → Φ ⊢Nf⋆ * → ∅ ⊢Nf⋆ *
+sig2type .∅ ∅ C = C
+sig2type (Φ ,⋆ J) (Γ ,⋆ J) C = sig2type Φ Γ (Π C)
+sig2type Φ        (Γ ,  A) C = sig2type Φ Γ (A ⇒ C)
 
-itype : ∀{Φ} → Builtin → Φ ⊢Nf⋆ *
-itype b = let Φ ,, Γ ,, C = ISIG b in subNf (λ()) (isig2type Φ Γ C)
+btype : ∀{Φ} → Builtin → Φ ⊢Nf⋆ *
+btype b = let Φ ,, Γ ,, C = sig b in subNf (λ()) (sig2type Φ Γ C)
 
-postulate itype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → itype b ≡ renNf ρ (itype b)
-postulate itype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → itype b ≡ subNf ρ (itype b)
+postulate btype-ren : ∀{Φ Ψ} b (ρ : ⋆.Ren Φ Ψ) → btype b ≡ renNf ρ (btype b)
+postulate btype-sub : ∀{Φ Ψ} b (ρ : SubNf Φ Ψ) → btype b ≡ subNf ρ (btype b)
 
 infixl 7 _·⋆_
 
@@ -221,7 +221,7 @@ data _⊢_ {Φ} (Γ : Ctx Φ) : Φ ⊢Nf⋆ * → Set where
       -------------------
     → Γ ⊢ con tcn
 
-  ibuiltin : (b :  Builtin) → Γ ⊢ itype b
+  builtin : (b :  Builtin) → Γ ⊢ btype b
 
   error : (A : Φ ⊢Nf⋆ *) → Γ ⊢ A
 \end{code}
@@ -265,5 +265,5 @@ ctx2bwdarity (Γ ,⋆ J) = ctx2bwdarity Γ :< Type
 ctx2bwdarity (Γ , A)  = ctx2bwdarity Γ :< Term
 
 arity : Builtin → Arity
-arity b = ctx2bwdarity (proj₁ (proj₂ (ISIG b))) <>> []
+arity b = ctx2bwdarity (proj₁ (proj₂ (sig b))) <>> []
 \end{code}

plutus-metatheory/src/Algorithmic/CC.lagda.md

@@ -188,7 +188,7 @@ stepT (E ▻ (M ·⋆ A))   = extEC E (-·⋆ A) ▻ M
 stepT (E ▻ wrap A B M) = extEC E wrap- ▻ M
 stepT (E ▻ unwrap M)   = extEC E unwrap- ▻ M
 stepT (E ▻ con c)      = E ◅ V-con c
-stepT (E ▻ ibuiltin b) = E ◅ ival b
+stepT (E ▻ builtin b)  = E ◅ ival b
 stepT (E ▻ error A)    = ◆ A
 stepT (E ◅ V)          = stepV V (dissect E)
 stepT (□ V)            = □ V
@@ -1045,8 +1045,8 @@ thm1b (wrap A B M) M' E p N V (step* refl q) =
 thm1b (unwrap M) M' E p N V (step* refl q) =
   thm1b M _ (extEC E unwrap-) (trans p (sym (extEC-[]ᴱ E unwrap- M))) N V q
 thm1b (con c) M' E p N V (step* refl q) = thm1bV (con c) (V-con c) M' E p N V q
-thm1b (ibuiltin b) M' E p N V (step* refl q) =
-  thm1bV (ibuiltin b) (ival b) M' E p N V q
+thm1b (builtin b) M' E p N V (step* refl q) =
+  thm1bV (builtin b) (ival b) M' E p N V q
 thm1b (error _) M' E p N V (step* refl q) = ⊥-elim (diamond2box N V q)
 
 thm1bV M W M' E p N V (step* x q) with dissect E | inspect dissect E

plutus-metatheory/src/Algorithmic/CEKV.lagda.md

@@ -71,7 +71,7 @@ data Value : (A : ∅ ⊢Nf⋆ *) → Set where
        → Value (Π B)
 
 data BAPP b where
-  base : BAPP b (start (arity b)) (itype b)
+  base : BAPP b (start (arity b)) (btype b)
   app : ∀{A B}{az as}
     → (p : az <>> (Term ∷ as) ∈ arity b)
     → BAPP b p (A ⇒ B)
@@ -125,7 +125,7 @@ dischargeBody⋆ {A = A} M ρ = conv⊢
   (sub (extsNf (ne ∘ `)) (exts⋆ (ne ∘ `) (env2ren ρ)) M)
 
 dischargeB : ∀{b A}{az}{as}{p : az <>> as ∈ arity b} → BAPP b p A → ∅ ⊢ A
-dischargeB {b = b} base = ibuiltin b
+dischargeB {b = b} base = builtin b
 dischargeB (app p bt vu) = dischargeB bt · discharge vu
 dischargeB (app⋆ p bt refl) = dischargeB bt ·⋆ _
 
@@ -816,7 +816,7 @@ data State (T : ∅ ⊢Nf⋆ *) : Set where
 
 
 
-ival : ∀ b → Value (itype b)
+ival : ∀ b → Value (btype b)
 ival addInteger = V-I⇒ addInteger _ base
 ival subtractInteger = V-I⇒ subtractInteger _ base
 ival multiplyInteger = V-I⇒ multiplyInteger _ base
@@ -878,7 +878,7 @@ step (s ; ρ ▻ (L ·⋆ A))        = (s , -·⋆ A) ; ρ ▻ L
 step (s ; ρ ▻ wrap A B L) = (s , wrap-) ; ρ ▻ L
 step (s ; ρ ▻ unwrap L) = (s , unwrap-) ; ρ ▻ L
 step (s ; ρ ▻ con c) = s ◅ V-con c
-step (s ; ρ ▻ ibuiltin b) = s ◅ ival b
+step (s ; ρ ▻ builtin b) = s ◅ ival b
 step (s ; ρ ▻ error A) = ◆ A
 step (ε ◅ V) = □ V
 step ((s , -· M ρ') ◅ V) = (s , V ·-) ; ρ' ▻ M
@@ -973,7 +973,7 @@ cek2ckClos (L ·⋆ A) ρ = cek2ckClos L ρ ·⋆ A
 cek2ckClos (wrap A B L) ρ = wrap A B (cek2ckClos L ρ)
 cek2ckClos (unwrap L) ρ = unwrap (cek2ckClos L ρ)
 cek2ckClos (con c) ρ = con c
-cek2ckClos (ibuiltin b) ρ = ibuiltin b
+cek2ckClos (builtin b) ρ = builtin b
 cek2ckClos (error _) ρ = error _
 
 cek2ckFrame : ∀{A B} → Frame A B → Red.Frame A B
@@ -1046,7 +1046,7 @@ thm65a (s ; ρ ▻ (L ·⋆ A)) s' (step* refl q) = CK.step* refl (thm65a _ s'
 thm65a (s ; ρ ▻ wrap A B L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
 thm65a (s ; ρ ▻ unwrap L) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
 thm65a (s ; ρ ▻ con c) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
-thm65a (s ; ρ ▻ ibuiltin b) s' (step* refl q) = CK.step* (ival-lem b) (thm65a _ s' q)
+thm65a (s ; ρ ▻ builtin b) s' (step* refl q) = CK.step* (ival-lem b) (thm65a _ s' q)
 thm65a (s ; ρ ▻ error _) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
 thm65a (ε ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
 thm65a ((s , -· L ρ) ◅ V) s' (step* refl q) = CK.step* refl (thm65a _ s' q)
@@ -1104,7 +1104,7 @@ postulate cek2ckClos-unwraplem : ∀{K}{A}{B : ∅ ⊢Nf⋆ K}{L : ∅ ⊢ μ A
 
 postulate cek2ckClos-conlem : ∀{tc : TyCon ∅}(c : TermCon (con tc)){Γ}{M' : Γ ⊢ con tc}{ρ : Env Γ} → con c ≡ cek2ckClos M' ρ → M' ≡ con c ⊎ ∃ λ x → M' ≡ ` x × V-con c ≡ lookup x ρ
 
-postulate cek2ckClos-ibuiltinlem : ∀{b}{Γ}{M' : Γ ⊢ itype b}{ρ : Env Γ} → ibuiltin b ≡ cek2ckClos M' ρ → (M' ≡ ibuiltin b × ∃ λ p → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (ival b)) ⊎ ∃ λ x → M' ≡ ` x × ∃ λ (p : ibuiltin b ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (lookup x ρ)
+postulate cek2ckClos-ibuiltinlem : ∀{b}{Γ}{M' : Γ ⊢ btype b}{ρ : Env Γ} → builtin b ≡ cek2ckClos M' ρ → (M' ≡ builtin b × ∃ λ p → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (ival b)) ⊎ ∃ λ x → M' ≡ ` x × ∃ λ (p : builtin b ≡ discharge (lookup x ρ)) → substEq Red.Value p (Red.ival b) ≡ cek2ckVal (lookup x ρ)
 
 cek2ckStack-εlem : ∀{A}(s : Stack A A) → CK.ε ≡ cek2ckStack s → s ≡ ε
 cek2ckStack-εlem ε       p = refl
@@ -1196,11 +1196,11 @@ thm65b {M = con c}{s = s}{M' = M'}{ρ = ρ}{s' = s'} p q (CK.step* refl r)
 ... | inj₁ refl = _ ,, step* refl r' ,, x1 ,, x2
 ... | inj₂ (var ,, refl ,, y2) = _ ,, step* (cong (s' ◅_) (sym y2)) r' ,, x1 ,, x2
 
-thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r)
+thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r)
   with cek2ckClos-ibuiltinlem {M' = N}{ρ = ρ} p
-thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y2 ,, y3) with thm65bV y2 y3 q r
+thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₂ (x ,, refl ,, y2 ,, y3) with thm65bV y2 y3 q r
 ... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
-thm65b {M = ibuiltin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₁ (refl ,, x1 ,, x2)
+thm65b {M = builtin b} {s = s}{M' = N}{ρ = ρ}{s' = s'} p q (CK.step* refl r) | inj₁ (refl ,, x1 ,, x2)
   with thm65bV x1 x2 q r
 ... | V' ,, r' ,, y1 ,, y2 = V' ,, step* refl r' ,, y1 ,, y2
 

plutus-metatheory/src/Algorithmic/CK.lagda.md

@@ -82,7 +82,7 @@ step ((s , (V-ƛ t ·-)) ◅ V)       = s ▻ (t [ discharge V ])
 step ((s , (-·⋆ A)) ◅ V-Λ t)      = s ▻ (t [ A ]⋆)
 step ((s , wrap-) ◅ V)            = s ◅ (V-wrap V)
 step ((s , unwrap-) ◅ V-wrap V)   = s ▻ deval V
-step (s ▻ ibuiltin b) = s ◅ ival b
+step (s ▻ builtin b) = s ◅ ival b
 step ((s , (V-I⇒ b {as' = []} p bt ·-)) ◅ vu) =
   s ▻ BUILTIN' b (bubble p) (app p bt vu)
 step ((s , (V-I⇒ b {as' = _ ∷ as'} p bt ·-)) ◅ vu) =
@@ -168,7 +168,7 @@ thm64 (E CC.▻ unwrap M) E' (CC.step* refl p) =
   step* (cong (λ E → E ▻ M) (lemmaH E unwrap-)) (thm64 _ E' p)
 thm64 (E CC.▻ con M) E' (CC.step* refl p) =
   step* refl (thm64 _ E' p)
-thm64 (E CC.▻ ibuiltin b) E' (CC.step* refl p) =
+thm64 (E CC.▻ builtin b) E' (CC.step* refl p) =
   step* refl (thm64 _ E' p)
 thm64 (E CC.▻ error _) E' (CC.step* refl p) = step* refl (thm64 _ E' p)
 thm64 (E CC.◅ V) E' (CC.step* refl p) with CC.dissect E | inspect CC.dissect E
@@ -197,7 +197,7 @@ thm64b (s ▻ (M ·⋆ A)) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (s ▻ wrap A B M) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (s ▻ unwrap M) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (s ▻ con c) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
-thm64b (s ▻ ibuiltin b) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
+thm64b (s ▻ builtin b) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (s ▻ error _) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (ε ◅ V) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b ((s , (-· M)) ◅ V) s' (step* refl p) = CC.step*
@@ -235,7 +235,7 @@ thm64b (□ x₁) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 thm64b (◆ A) s' (step* refl p) = CC.step* refl (thm64b _ s' p)
 
 test : State (con unit)
-test = ε ▻ (ƛ (con unit) · (ibuiltin iData · con (integer (+ 0))))
+test = ε ▻ (ƛ (con unit) · (builtin iData · con (integer (+ 0))))
 
 postulate
   lemV : ∀{A B}(M : ∅ ⊢ B)(V : Value M)(E : Stack A B) → (E ▻ M) -→s (E ◅ V)

plutus-metatheory/src/Algorithmic/Completeness.lagda

@@ -112,7 +112,7 @@ nfList : ∀{Δ} → List (Δ ⊢⋆ *) → List (Δ ⊢Nf⋆ *)
 nfList []       = []
 nfList (A ∷ As) = nf A ∷ nfList As
 
-postulate itype-lem : ∀ {Φ} b → Norm.itype {Φ} b ≡ nf (Syn.itype b)
+postulate btype-lem : ∀ {Φ} b → Norm.btype {Φ} b ≡ nf (Syn.btype b)
 
 nfType : ∀{Φ Γ}
   → {A : Φ ⊢⋆ *}
@@ -137,7 +137,7 @@ nfType (Syn.unwrap {A = A}{B = B} t) = Norm.conv⊢
   (Norm.unwrap (nfType t))
 nfType (Syn.conv p t) = Norm.conv⊢ refl (completeness p) (nfType t)
 nfType (Syn.con t) = Norm.con (nfTypeTC t)
-nfType (Syn.ibuiltin b) = Norm.conv⊢ refl (itype-lem b) (Norm.ibuiltin b)
+nfType (Syn.builtin b) = Norm.conv⊢ refl (btype-lem b) (Norm.builtin b)
 nfType (Syn.error A) = Norm.error (nf A)
 
 completenessT : ∀{Φ Γ}{A : Φ ⊢⋆ *} → Γ Syn.⊢ A

plutus-metatheory/src/Algorithmic/Erasure.lagda

@@ -67,7 +67,7 @@ erase (_·⋆_ t A)           = force (erase t)
 erase (wrap A B t)         = erase t
 erase (unwrap t)           = erase t
 erase {Γ = Γ} (con t)      = con (eraseTC {Γ = Γ} t)
-erase (ibuiltin b)         = builtin b
+erase (builtin b)          = builtin b
 erase (error A)            = error
 \end{code}
 
@@ -269,9 +269,9 @@ same {Γ = Γ} (D.con tcn) = trans
   (cong con (sameTC {Γ = Γ} tcn))
   (lemcon' (lenLemma Γ) (eraseTC {Γ = nfCtx Γ} (nfTypeTC tcn)))
 
-same {Γ = Γ} (D.ibuiltin b) = trans
+same {Γ = Γ} (D.builtin b) = trans
   (lembuiltin b (lenLemma Γ)) (cong (subst _⊢ (lenLemma Γ))
-  (lem-erase refl (itype-lem b) (ibuiltin b)))
+  (lem-erase refl (btype-lem b) (builtin b)))
 same {Γ = Γ} (D.error A) = lemerror (lenLemma Γ)
 
 open import Algorithmic.Soundness
@@ -326,6 +326,6 @@ same' {Γ = Γ} (unwrap t) = same' t
 same' {Γ = Γ} (con x) = trans
   (cong con (same'TC {Γ = Γ} x))
   (lemcon' (same'Len Γ) (D.eraseTC {Γ = embCtx Γ}(embTC x)))
-same' {Γ = Γ} (ibuiltin b) = lembuiltin b (same'Len Γ)
+same' {Γ = Γ} (builtin b) = lembuiltin b (same'Len Γ)
 same' {Γ = Γ} (error A) = lemerror (same'Len Γ)
 \end{code}