chore: fix tests
This commit is contained in:
parent
e45211f31c
commit
a5cf1ac5ae
3 changed files with 4 additions and 4 deletions
|
|
@ -8,4 +8,4 @@ if strictOr (C == 0) (spin b) then "hello"
|
|||
else "world"
|
||||
|
||||
def main (xs : List String) : IO Unit :=
|
||||
IO.println (f xs.head!.toNat)
|
||||
IO.println (f 0)
|
||||
|
|
|
|||
|
|
@ -3,6 +3,6 @@ phashmap_inst_coherence.lean:11:0: error: type mismatch at application
|
|||
term
|
||||
m
|
||||
has type
|
||||
@PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat Nat.DecidableEq)
|
||||
@PersistentHashMap Nat Nat Nat.Hashable (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b))
|
||||
but is expected to have type
|
||||
@PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat Nat.DecidableEq)
|
||||
@PersistentHashMap Nat Nat natDiffHash (@beqOfEq Nat (λ (ab : Nat), Nat.DecidableEq a b))
|
||||
|
|
|
|||
|
|
@ -62,7 +62,7 @@ def hasDecEq : ∀ (a b : Nat), Decidable (a = b)
|
|||
| isFalse xney => isFalse (fun h => Nat.noConfusion h (fun xeqy => absurd xeqy xney))
|
||||
|
||||
instance : DecidableEq ℕ :=
|
||||
{decEq := hasDecEq}
|
||||
hasDecEq
|
||||
|
||||
def repeat.{u} {α : Type u} (f : ℕ → α → α) : ℕ → α → α
|
||||
| 0, a => a
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue