Skip to content

T13910 is broken in optasm

Compile failed (exit code 1) errors were:
*** Core Lint errors : in result of Simplifier ***
<no location info>: warning:
    In the type ‘forall t (from :: t) (to :: t) (p :: t -> *).
                 App t (':->) * (p |> Sym (D:R:Funk1:->k2[0] <t>_N <*>_N)) from
                 -> (from :~: to)
                 -> WhyReplacePoly
                      (':->)
                      from
                      (p |> Sym (D:R:Funk1:->k2[0] <t>_N <*>_N))
                      to
                      ('Refl |> ((:~:) <t>_N <from>_N (Sym co_a5yh))_N)’
    co_a5yh :: to_a5vA ~# from_a5vz
    [LclId[CoVarId]] is out of scope
*** Offending Program ***
...
Edited by Ben Gamari
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information