Skip to content

Commit

Permalink
Update plutus-metatheory/src/VerifiedCompilation/UCaseOfCase.lagda.md
Browse files Browse the repository at this point in the history
Co-authored-by: effectfully <effectfully@gmail.com>
  • Loading branch information
ramsay-t and effectfully committed May 3, 2024
1 parent c300c78 commit 91db1ac
Showing 1 changed file with 1 addition and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ data _⊢̂_⊳̂_ (X : Set) : (X ⊢) → (X ⊢) → Set where
→ All (λ altpair → X ⊢̂ (proj₁ altpair) ⊳̂ (proj₂ altpair)) (zip alts alts') -- recursive translation for the other case patterns
→ X ⊢̂ p ⊳̂ p'
------------------------
→ X ⊢̂ case p alts ⊳̂ case p alts'
→ X ⊢̂ case p alts ⊳̂ case p' alts'
builtin : ∀ {b : Builtin} → X ⊢̂ builtin b ⊳̂ builtin b
error : X ⊢̂ error ⊳̂ error
Expand Down

0 comments on commit 91db1ac

Please sign in to comment.