blob: 4d9ec334cbfd0dda86cfe92d8c526e1b422458c8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
{-# OPTIONS --without-K --safe #-}
module Data.Util where
open import Data.List using (List)
open import Data.List.Membership.Propositional using (_∉_)
open import Data.Nat using (ℕ)
record IsFresh (mkFresh : List ℕ → ℕ) : Set where
field
distinct : ∀ αs → mkFresh αs ∉ αs
open IsFresh public
|
