proger
/ TypeSystem.v
Created
June 23, 2016 22:42
— forked from alpicola/TypeSystem.v
Strong Normalization for STLC
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Require Import Coq.Unicode.Utf8 Arith FunctionalExtensionality String Coq.Program.Equality. | |
| Set Implicit Arguments. | |
| Ltac invert H := inversion H; clear H; subst. | |
| Ltac invert1 H := invert H; []. | |
| Inductive star A (R : A -> A -> Prop) : A -> A -> Prop := | |
| | StarRefl : forall x, | |
| star R x x |
proger
/ prior_likelihood_conflict.r
Created
September 12, 2023 10:09
— forked from rmcelreath/prior_likelihood_conflict.r
Demonstration of how normal and student-t distributions interact in Bayesian updating
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # prior - likelihood conflict | |
| library(rethinking) | |
| yobs <- 0 | |
| mtt <- ulam( | |
| alist( | |
| y ~ dstudent(2,mu,1), | |
| mu ~ dstudent(2,10,1) |