Skip to content

Commit c25c581

Browse files
committed
migrate new Computational.{agda,lagda.md} files
1 parent a3839f0 commit c25c581

File tree

2 files changed

+14
-0
lines changed

2 files changed

+14
-0
lines changed

src/Ledger/Conway/Specification/PoolReap/Properties/Computational.lagda.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Conway/Specification/PoolReap/Properties/Computational.lagda.md
4+
---
5+
6+
```agda
17
{-# OPTIONS --safe #-}
28
39
open import Ledger.Conway.Specification.Transaction
@@ -35,3 +41,4 @@ POOLREAP-deterministic-≡ : ∀ {prs' prs'' e e' prs''' prs''''}
3541
→ _ ⊢ prs'' ⇀⦇ e' ,POOLREAP⦈ prs''''
3642
→ prs''' ≡ prs''''
3743
POOLREAP-deterministic-≡ refl refl = POOLREAP-deterministic
44+
```

src/Ledger/Conway/Specification/Rewards/Properties/Computational.lagda.md

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,9 @@
1+
---
2+
source_branch: master
3+
source_path: src/Ledger/Conway/Specification/Rewards/Properties/Computational.lagda.md
4+
---
5+
6+
```agda
17
{-# OPTIONS --safe #-}
28
39
open import Ledger.Prelude
@@ -23,3 +29,4 @@ module _ {lstate : LState} {ss : Snapshots} where
2329
→ lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'
2430
→ lstate ⊢ ss ⇀⦇ tt ,SNAP⦈ ss'' → ss' ≡ ss''
2531
SNAP-deterministic SNAP SNAP = refl
32+
```

0 commit comments

Comments
 (0)