Changing <-rec to use _<_ instead of _<'_

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
module NatLess where

open import Data.Nat
open import Data.Nat.Properties

import Induction.Nat as WF<
import Induction.WellFounded as WF

-- ≤⇒≤′ comes from Data.Nat.Properties
open WF.Subrelation {_<_ = _<_} 

module _ {} where
  open WF.All (well-founded WF<.<-well-founded)  public
    renaming (wfRec to <-rec)

-- <-rec now works with _<_