File: github1794.v

package info (click to toggle)
coq-hott 9.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid, trixie
  • size: 6,440 kB
  • sloc: sh: 452; python: 414; haskell: 125; makefile: 21
file content (6 lines) | stat: -rw-r--r-- 431 bytes parent folder | download | duplicates (3) 
1
2
3
4
5
6
 
From HoTT Require Import Basics.Overture.

(** When [rewrite] is first used, it defines helper lemmas.  If the first use is in a Section that has universe variables, then these lemmas get unnecessary universe variables.  Overture uses [rewrite] outside of a section to ensure that they have the expected number of universe variables, and we test that here. *)

Check internal_paths_rew@{u1 u2}.
Check internal_paths_rew_r@{u1 u2}.