Skip to content

Commit

Permalink
Compatibility with stdlib 2.1
Browse files Browse the repository at this point in the history
  • Loading branch information
WhatisRT committed Jun 24, 2024
1 parent e834cf7 commit ac10c5a
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion MetaPrelude.agda
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ open import Data.List hiding (align; alignWith; fromMaybe; map; zip; zipWith) pu
open import Data.Maybe hiding (_>>=_; ap; align; alignWith; fromMaybe; map; zip; zipWith) public
open import Data.Unit hiding (_≟_) public
open import Data.Sum hiding (assocʳ; assocˡ; map; map₁; map₂; reduce; swap) public
open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip) public
open import Data.Product hiding (assocʳ; assocˡ; map; map₁; map₂; swap; zip; zipWith) public
open import Data.Nat hiding (_≟_; _≤_; _≤?_; _<_; _<?_; _≤ᵇ_; _≡ᵇ_) public
open import Data.String using (String; _<+>_) public

Expand Down
2 changes: 1 addition & 1 deletion Tactic/Derive/TestTypes.agda
Original file line number Diff line number Diff line change
Expand Up @@ -77,7 +77,7 @@ open import Data.Unit using (⊤) public
open import Data.Universe using (Universe) public
open import Data.Vec using (Vec) public
open import Data.W using (W) public
open import Data.Word using (Word64) public
open import Data.Word64 using (Word64) public

stdlibTypes : List Name
stdlibTypes = quote Bool ∷ quote Container ∷ quote Fin ∷ quote ℤ ∷ quote List ∷ quote Maybe ∷ quote ℕ ∷ quote Σ ∷ quote ℚ ∷ quote Record ∷ quote Refinement ∷ quote Sign ∷ quote _⊎_ ∷ quote These ∷ quote ⊤ ∷ quote Universe ∷ quote Vec ∷ quote W ∷ []

0 comments on commit ac10c5a

Please sign in to comment.