-
- Downloads
move the embedding primitive to upred
Showing
- _CoqProject 1 addition, 1 deletion_CoqProject
- iris/base_logic/bi.v 53 additions, 0 deletionsiris/base_logic/bi.v
- iris/base_logic/lib/monpred_si_embed.v 27 additions, 0 deletionsiris/base_logic/lib/monpred_si_embed.v
- iris/base_logic/lib/si_embed.v 0 additions, 98 deletionsiris/base_logic/lib/si_embed.v
- iris/base_logic/upred.v 43 additions, 0 deletionsiris/base_logic/upred.v
- iris/bi/embedding.v 1 addition, 0 deletionsiris/bi/embedding.v
Loading
Please register or sign in to comment