search

stefan-hoeck / idris2-elab-util

Utilities and documentation for exploring idirs2's new elaborator reflection.
BSD 2-Clause "Simplified" License
76 stars 16 forks source link

[ refactor ] generalize parameter handling #70

Closed stefan-hoeck closed 1 year ago

stefan-hoeck commented 1 year ago

Motivation for this change: The following did not work so far, because the (implicit) type argument k was not set explicitly in derived elaborator scripts:

record Id (v : k) where
  constructor MkId
  value : Nat

namespace Id
  %runElab derive "Id" [Show,Eq,Ord,FromInteger]

With this PR, handling implicit type constructor arguments has been fixed. Auto-implicit type constructor arguments are still being ignored. I'll have to think about those some more.