Skip to content

Commit 97d8b82

Browse files
committed
feat: add compatibility wrappers for core modules
This commit adds compatibility wrappers for Echo, EchoCharacteristic, and EchoResidue to prevent breaking external dependencies.
1 parent 6b0a5b3 commit 97d8b82

3 files changed

Lines changed: 15 additions & 0 deletions

File tree

proofs/agda/Echo.agda

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
module Echo where
4+
5+
open import Echo.Core public
Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
module EchoCharacteristic where
4+
5+
open import Echo.Characteristic public

proofs/agda/EchoResidue.agda

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{-# OPTIONS --safe --without-K #-}
2+
3+
module EchoResidue where
4+
5+
open import Echo.Residue public

0 commit comments

Comments
 (0)