We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 20d5846 commit a60eefbCopy full SHA for a60eefb
src/Induction/WellFounded.agda
@@ -11,8 +11,8 @@ module Induction.WellFounded where
11
open import Data.Product.Base using (Σ; _,_; proj₁; proj₂)
12
open import Function.Base using (_∘_; flip; _on_)
13
open import Induction
14
- using (RecStruct; RecursorBuilder; Recursor; build; SubsetRecursorBuilder
15
- ; SubsetRecursor; subsetBuild)
+ using (RecStruct; RecursorBuilder; Recursor; build
+ ; SubsetRecursorBuilder; SubsetRecursor; subsetBuild)
16
open import Level using (Level; _⊔_)
17
open import Relation.Binary.Core using (Rel)
18
open import Relation.Binary.Definitions
0 commit comments