Skip to content
Snippets Groups Projects

Adding kinded polymorphism in types

Adding kinded polymorphism in types
jonas/kinded_polymorphism into master
1 unresolved thread
Merged Jonas Kastberg requested to merge jonas/kinded_polymorphism into master
1 unresolved thread

Merge request reports

Loading
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
theories/logrel/model.v 0 → 100644
126
127 Global Instance kind_interp_inhabited k : Inhabited (kind_interp k Σ).
128 Proof.
129 destruct k.
130 - apply (populate (Lty inhabitant)).
131 - apply (populate (Lsty inhabitant)).
132 Qed.
133
134 End lty_ofe.
135
136 Arguments kind_interpO : clear implicits.
137
138 Notation ltyO Σ := (kind_interpO Σ ty_kind).
139 Notation lstyO Σ := (kind_interpO Σ sty_kind).
140
141 (* Typing for operators *)
  • Jonas Kastberg unmarked as a Work In Progress

    unmarked as a Work In Progress

  • Jonas Kastberg mentioned in commit 4e372fb3

    mentioned in commit 4e372fb3

  • Jonas Kastberg merged

    merged

    • Please register or sign in to reply