Yiyun Liu issues

Repositories
Issues
Comments

Results 12 issues of


                                            Yiyun Liu

CoreToLogic: and/or embedding is broken

I encountered this issue when trying to reuse coreToLogic to turn the elaborated core expression back to fixpoint expression. ```haskell {-@ LIQUID "--reflect" @-} {-@ reflect bad @-} bad ::...

Anomaly "in Univ.repr: Universe file.v.1700 undefined."

Here's my best effort attempt at minimizing the example: ```coq From Equations Require Import Equations. Inductive Ki : Type := | Star : Ki. Inductive Ty : Type := |...