23 lines
954 B
Text
23 lines
954 B
Text
def h : BV 32 → Array Bool :=
|
|
fun (x : BV 32) => (fun (x : BV 32) => g (f x).val) x
|
|
def r : Nat → Prop :=
|
|
fun (a : Nat) => if a == 0 = true then a != 1 = true else a != 2 = true
|
|
def r : Nat → Prop :=
|
|
fun a =>
|
|
@ite.{1} Prop
|
|
(@Eq.{1} Bool
|
|
(@BEq.beq.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a
|
|
(@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
|
|
Bool.true)
|
|
(instDecidableEqBool
|
|
(@BEq.beq.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a
|
|
(@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0)))
|
|
Bool.true)
|
|
(@Eq.{1} Bool
|
|
(@bne.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a (@OfNat.ofNat.{0} Nat 1 (instOfNatNat 1)))
|
|
Bool.true)
|
|
(@Eq.{1} Bool
|
|
(@bne.{0} Nat (@instBEq.{0} Nat fun a b => instDecidableEqNat a b) a (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
|
|
Bool.true)
|
|
def s : Option Nat :=
|
|
ConstantFunction.f myFun 3 <|> ConstantFunction.f myFun 4
|