mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-12-24 04:09:10 +03:00
1b695bcc52
This is particularly important if we're generating something that needs to be parsed and checked again. Fixes #185
14 lines
331 B
Idris
14 lines
331 B
Idris
data BNat = BZ | O BNat | E BNat
|
|
|
|
bnat_ind : {0 p : BNat -> Type}
|
|
-> p BZ
|
|
-> ((bn : BNat) -> p bn -> p (O bn))
|
|
-> ((bn : BNat) -> p bn -> p (E bn))
|
|
-> (bn : BNat) -> p bn
|
|
bnat_ind pbz po pe = go
|
|
where
|
|
go : (bn : BNat) -> p bn
|
|
go BZ = ?pbz_hole
|
|
go (O x) = po x (go x)
|
|
go (E x) = pe x (go x)
|