Justus Matthiesen
Results
3
issues of
Justus Matthiesen
# Example Elaboration of a record that has an implicit function as one of its parameters ```idris record R (A : Type) (B : {a : A} -> Type) where...
Take the program ```idris %default total record Box where constructor MkBox unbox : Nat replace : (b : Box) -> (k : Nat) -> unbox b === k -> Box...