diff options
| author | Josh Chen | 2018-08-18 21:28:21 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-18 21:28:21 +0200 |
| commit | e1be5f97bb2a42b3179bc24b118d69af137f8e5d (patch) | |
| tree | 37fa2dacc40261bf37726e23121df0ba5b9af68e /ex/Synthesis.thy | |
| parent | 03c734ea067bd28210530d862137133e2215ca80 (diff) | |
Regrouping type rules
Diffstat (limited to 'ex/Synthesis.thy')
| -rw-r--r-- | ex/Synthesis.thy | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/ex/Synthesis.thy b/ex/Synthesis.thy index e5a8ecf..cff9374 100644 --- a/ex/Synthesis.thy +++ b/ex/Synthesis.thy @@ -1,6 +1,5 @@ (* Title: HoTT/ex/Synthesis.thy Author: Josh Chen - Date: Aug 2018 Examples of synthesis. *) @@ -33,8 +32,8 @@ text " schematic_goal "?p`0 \<equiv> 0" and "\<And>n. n: \<nat> \<Longrightarrow> (?p`(succ n)) \<equiv> n" apply compute prefer 4 apply compute -prefer 3 apply (rule Nat_rules) -apply (rule Nat_rules | assumption)+ +prefer 3 apply compute +apply (rule Nat_routine Nat_elim | assumption)+ done text " @@ -52,7 +51,7 @@ proof (simple lems: pred_type) proof compute show "\<And>n. n: \<nat> \<Longrightarrow> ind\<^sub>\<nat> (\<lambda>a b. a) 0 n: \<nat>" by simple show "ind\<^sub>\<nat> (\<lambda>a b. a) 0 0 \<equiv> 0" - proof (rule Nat_comps) + proof compute show "\<nat>: U(O)" .. qed simple qed rule |